p-automata: acceptors for Markov Chains

We present p-automata, which accept an entire Markov chain as input. Acceptance is determined by solving a sequence of stochastic weak and weak games. The set of languages of Markov chains obtained in this way is closed under Boolean operations. Language emptiness and containment are equi-solvable, and languages themselves are closed under bisimulation. A Markov chain (respectively, PCTL formula) determines a p-automaton whose language is the bisimulation equivalence class of that Markov chain (respectively, the set of models of that formula). We define a simulation game between p-automata, decidable in EXPTIME. Simulation under-approximates language containment, whose decidability status is presently unknown