Computing Publications

Publications Home » p-Automata: New Foundations for D...

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

Michael Huth, Nir Piterman, Daniel Wagner

Conference or Workshop Paper
QEST 2010, 7th International Conference on Quantitative Evaluation of Systems
September, 2010
IEEE Computer Society
DOI 10.1109/QEST.2010.29

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.

PDF of full publication (462 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.