Deductive Controller Synthesis for Probabilistic Hyperproperties

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU149418" target="_blank" >RIV/00216305:26230/23:PU149418 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-031-43835-6_20" target="_blank" >http://dx.doi.org/10.1007/978-3-031-43835-6_20</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-43835-6_20" target="_blank" >10.1007/978-3-031-43835-6_20</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Deductive Controller Synthesis for Probabilistic Hyperproperties

Popis výsledku v původním jazyce

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms&nbsp;HYPERPROB, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g.&nbsp;partial observability) as well as inter-controller constraints (e.g.&nbsp;agreements on a common action).

Název v anglickém jazyce

Deductive Controller Synthesis for Probabilistic Hyperproperties

Popis výsledku anglicky

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms&nbsp;HYPERPROB, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g.&nbsp;partial observability) as well as inter-controller constraints (e.g.&nbsp;agreements on a common action).

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Quantitative Evaluation of SysTems

ISBN

978-3-031-43834-9

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

288-306

Název nakladatele

Springer Verlag

Místo vydání

Cham

Místo konání akce

Antwerp

Datum konání akce

20. 9. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—