Publication Details

Deductive Controller Synthesis for Probabilistic Hyperproperties

ANDRIUSHCHENKO, R.; BARTOCCI, E.; ČEŠKA, M.; FRANCESCO, P.; SARAH, S. Deductive Controller Synthesis for Probabilistic Hyperproperties. In Quantitative Evaluation of SysTems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Cham: Springer Verlag, 2023. p. 288-306. ISBN: 978-3-031-43834-9.
Czech title
Syntéza konroléru pro pravděpodobnostní hyper-vlastnosti
Type
conference paper
Language
English
Authors
Andriushchenko Roman, Ing. (DITS)
BARTOCCI, E.
Češka Milan, doc. RNDr., Ph.D. (DITS)
FRANCESCO, P.
SARAH, S.
Keywords

Hyperproperties, Markov decision processes, abstraction refinement

Abstract

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 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. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).

Published
2023
Pages
288–306
Proceedings
Quantitative Evaluation of SysTems
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume
14287
ISBN
978-3-031-43834-9
Publisher
Springer Verlag
Place
Cham
DOI
EID Scopus
BibTeX
@inproceedings{BUT185191,
  author="ANDRIUSHCHENKO, R. and BARTOCCI, E. and ČEŠKA, M. and FRANCESCO, P. and SARAH, S.",
  title="Deductive Controller Synthesis for Probabilistic Hyperproperties",
  booktitle="Quantitative Evaluation of SysTems",
  year="2023",
  series="Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
  volume="14287",
  pages="288--306",
  publisher="Springer Verlag",
  address="Cham",
  doi="10.1007/978-3-031-43835-6\{_}20",
  isbn="978-3-031-43834-9"
}
Back to top