Model Checking Probabilistic Pushdown Automata
by
Javier Esparza,
Antonín Kučera,
Richard Mayr,
A full version of the paper presented at LICS`04. July 2004, 34 pages.
FIMU-RS-2004-03.
Available as Postscript,
PDF.
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 Buchi automata, and show
that both qualitative and quantitative model checking for pPDA is
decidable.