p-Automata and Obligation Games

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 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.