p-Automata and Obligation Games

Nir Piterman
University of Leicester
Friday, 26 October, 2012 - 14:00
"Rotule" 2NO8.08 (eighth floor)

We present our automata-based approach to probabilistic verification. This new approach adapts notions and techniques from alternating tree automata to the realm of Markov chains. The resulting p-automata determine languages of Markov chains. In order to determine acceptance of Markov chains by p-automata we develop a new notion of games, which we call \emph{obligation games}. Intuitively, one player commits to achieving a certain probability of winning in the interaction.

We survey the initial results regarding obligation games and p-automata. These include algorithms for solving obligation parity games, initial results about the expressive power of p-automata, and the relation between p-automata and pCTL model checking. In particular, these initial foundations show that p-automata enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics.

Many interesting questions remain open. For example, further algorithmic studies of obligation games, the theory of p-automata, and the usage in practice of p-automata as an abstraction framework for Markov chains.

Joint work with: Krishnendu Chatterjee, Michael Huth, and Daniel Wagner.