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.