##
p-Automata: New Foundations for Discrete-Time Probabilistic Verification

### Nir Piterman

We develop a new approach to probabilistic verification by adapting
notions and techniques from alternating tree automata to the realm of
Markov chains. The resulting p-automata determine languages of Markov
chains which are proved to be closed under Boolean operations, to
subsume bisimulation equivalence classes of Markov chains, and to
subsume the set of models of any PCTL formula.

Our acceptance game for an input Markov chain to a p-automata is shown
to be well-defined and to be in EXPTIME in general; but its complexity
is that of PCTL model checking for automata that represent PCTL
formulas. We also derive a notion of simulation between p-automata
that approximates language containment in EXPTIME.

These foundations therefore enable abstraction-based probabilistic
model checking
for probabilistic specifications that subsume Markov chains, and LTL
and CTL* like logics.

Joint work with M. Huth and D. Wagner