DocumentCode :
2550611
Title :
p-Automata: New Foundations for Discrete-Time Probabilistic Verification
Author :
Huth, Michael ; Piterman, Nir ; Wagner, Daniel
Author_Institution :
Dept. of Comput., Imperial Coll. London, London, UK
fYear :
2010
fDate :
15-18 Sept. 2010
Firstpage :
161
Lastpage :
170
Abstract :
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.
Keywords :
Boolean algebra; Markov processes; automata theory; probability; Boolean operations; Markov chains; discrete time probabilistic verification; p-automata; tree automata; Automata; Computational modeling; Gallium; Games; Markov processes; Probabilistic logic; Markov chains; automata; checking abstraction; model;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Quantitative Evaluation of Systems (QEST), 2010 Seventh International Conference on the
Conference_Location :
Williamsburg, VA
Print_ISBN :
978-1-4244-8082-1
Type :
conf
DOI :
10.1109/QEST.2010.29
Filename :
5600391
Link To Document :
بازگشت