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