Wednesday, February 28, 19:00: L’Osteria
Thursday, February 29, 18:00: Papa Rossi

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

Probabilistic Hyperproperties of Markov Decision Processes:

Probabilistic temporal logics such as PCTL and PCTL*, which extend branching temporal logics with a probabilistic quantifier, are an established formalism for specifying performance and reliability requirements of concurrent probabilistic systems. They are, however, not capable of expressing many interesting requirements, such as, for example, probabilistic noninterference. More generally, they cannot capture probabilistic hyperproperties, which relate multiple executions of a system. Hyperproperties 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 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.

Barbara König, Universität Duisburg Essen

Approximating Fixpoints of Approximated Functions:

There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration.
It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions.
After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated.
We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions.
We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints.