Model Checking Probabilistic Pushdown Automata

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 check...

Full description

Bibliographic Details
Main Authors: Javier Esparza, Antonin Kucera, Richard Mayr
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2006-03-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/2256/pdf