Publication Details
Deductive Controller Synthesis for Probabilistic Hyperproperties
BARTOCCI, E.
Češka Milan, doc. RNDr., Ph.D. (DITS)
FRANCESCO, P.
SARAH, S.
Hyperproperties, Markov decision processes, abstraction refinement
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).
@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"
}