Name
Abstract | ||
|---|---|---|
We introduce p-Automata, which are automata that accept languages of Markov chains, by adapting notions and techniques from alternating tree automata to the realm of Markov chains. The set of languages of p-automata is closed under Boolean operations, and for every PCTL formula it contains the language of the set of models of the formula. Furthermore, the language of every p-automaton is closed under probabilistic bisimulation. Similar to tree automata, whose acceptance is defined via two-player games, we define acceptance of Markov chains by p-automata through two-player stochastic games. We show that acceptance is solvable in EXPTIME; but for automata that arise from PCTL formulas acceptance matches that of PCTL model checking, namely, linear in the formula and polynomial in the Markov chain. We also derive a notion of simulation between p-automata that approximates language containment in EXPTIME and is complete for Markov chains. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.peva.2012.05.005 | Perform. Eval. |
Keywords | Field | DocType |
pctl formulas acceptance,probabilistic model checking,language containment,pctl formula,discrete-time probabilistic verification,subsume markov chain,tree automaton,markov chain,probabilistic specification,probabilistic bisimulation,pctl model checking,new foundation,probabilistic computation tree logic,game theory,markov chains | Discrete mathematics,Quantum finite automata,Model checking,EXPTIME,Computer science,Markov model,Markov chain,Probabilistic CTL,Theoretical computer science,Variable-order Markov model,Probabilistic logic,Distributed computing | Journal |
Volume | Issue | ISSN |
69 | 7-8 | 0166-5316 |
Citations | PageRank | References |
1 | 0.36 | 32 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Huth | 1 | 18 | 1.68 |
| Nir Piterman | 2 | 1154 | 70.02 |
| Daniel Wagner | 3 | 156 | 11.44 |