|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Model Checking Probabilistic Pushdown Automata |
| Authors:
J. Esparza
; A. Kucera
; Richard Mayr
|
| Date:Mar 2006 |
| Publication Title:Logical Methods in Computer Science |
|
Publication Type:Internet Publication
Publication Status:Published
|
|
|
|
DOI:10.2168/LMCS-2(1:2)2006
|
- Abstract:
- We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class or properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.
- Links To Paper
- 1st link
- Bibtex format
- @Misc{EDI-INF-RR-1197,
- author = {
J. Esparza
and A. Kucera
and Richard Mayr
},
- title = {Model Checking Probabilistic Pushdown Automata},
- year = 2006,
- month = {Mar},
- howpublished={Internet Publication},
- doi = {10.2168/LMCS-2(1:2)2006},
- url = {http://arxiv.org/pdf/cs.LO/0508003},
- note = {Logical Methods in Computer Science},
- }
|
