Past Event: Oden Institute Seminar

Probabilistic Hyperproperties of Markov Decision Processes ** Zoom Only**

Rayna Dimitrova, CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Abstract

Hyperproperties describe the correctness of a system as a relation between multiple executions. They generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. In this talk I will present a recently introduced temporal logic for the specification of hyperproperties of Markov decision processes (MDPs), called Probabilistic Hyper Logic (PHL). PHL extends classic probabilistic logics with quantification over schedulers and traces. It can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference and differential privacy, as well as novel applications in areas such as planning. A consequence of the generality of the logic is that the model checking problem for PHL is undecidable. I will present methods both for proving and for refuting formulas from a fragment of the logic that includes many probabilistic hyperproperties of interest.

 

**This seminar will be presented via ZOOM only.**

Biography

Rayna Dimitrova is a tenure-track faculty member at CISPA Helmholtz Center for Information Security in Saarbrücken, Germany. Her research is focused on the specification, verification, and synthesis of reactive systems. She primarily investigates quantitative versions of these questions, centered around the aspect of uncertainty in system and environment models. She is particularly interested in applications of formal methods to autonomous systems. Before joining CISPA, Rayna was a Lecturer (Assistant Professor) at the University of Sheffield, UK and at the University of Leicester, UK before that. Prior to that, she held postdoctoral positions at the University of Texas at Austin, and at the Max Planck Institute for Software Systems in Germany. She completed her PhD at Saarland University in Germany.