Gastvortrag: Francesco Pontiggia: Deductive Controller Synthesis for Probabilistic Hyperproperties

Montag, 13. November 2023, 11 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragender: Francesco Pontiggia



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. In my talk, I will describe our recent progresses to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. In particular, I will focus on a deductive method based on an abstraction refinement strategy tailored to the comparison of (probabilities of) multiple, different computation trees. Building on top of the logic HyperPCTL, it is the first approach that is also able to effectively integrate additional qualitative (or structural) constraints over the synthesized controllers. Finally, I will show some experiments and numbers we have obtained with a prototype implementation in the tool HyperPAYNT, comparing it with HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL.