Model checking probabilistic pushdown automata

Javier Esparza; Antonín Kučera; Richard Mayr

doi:10.1109/lics.2004.1319596

Model checking probabilistic pushdown automata

Javier Esparza, Antonín Kučera, Richard Mayr

Research output: Contribution to journal › Conference article › peer-review

81 Scopus citations

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 of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Büchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

Original language	English
Pages (from-to)	12-21
Number of pages	10
Journal	Proceedings - Symposium on Logic in Computer Science
Volume	19
DOIs	https://doi.org/10.1109/lics.2004.1319596
State	Published - 2004
Externally published	Yes
Event	Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science - Turku, Finland Duration: 13 Jul 2004 → 17 Jul 2004

Access to Document

10.1109/lics.2004.1319596

Cite this

@article{c170646bf04241c3bcd23d4abed70fdc,

title = "Model checking probabilistic pushdown automata",

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 of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic B{\"u}chi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.",

author = "Javier Esparza and Anton{\'i}n Ku{\v c}era and Richard Mayr",

year = "2004",

doi = "10.1109/lics.2004.1319596",

language = "English",

volume = "19",

pages = "12--21",

journal = "Proceedings - Symposium on Logic in Computer Science",

issn = "1043-6871",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

note = "Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science ; Conference date: 13-07-2004 Through 17-07-2004",

}

TY - JOUR

T1 - Model checking probabilistic pushdown automata

AU - Esparza, Javier

AU - Kučera, Antonín

AU - Mayr, Richard

PY - 2004

Y1 - 2004

N2 - 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 of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Büchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

AB - 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 of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Büchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

UR - http://www.scopus.com/inward/record.url?scp=4544326530&partnerID=8YFLogxK

U2 - 10.1109/lics.2004.1319596

DO - 10.1109/lics.2004.1319596

M3 - Conference article

AN - SCOPUS:4544326530

SN - 1043-6871

VL - 19

SP - 12

EP - 21

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

T2 - Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science

Y2 - 13 July 2004 through 17 July 2004

ER -

Model checking probabilistic pushdown automata

Abstract

Access to Document

Other files and links

Fingerprint

Cite this