Oxford logo
[BBF09] T. Brázdil, V. Brožek and V. Forejt. Branching-Time Model-Checking of Probabilistic Pushdown Automata. Electronic Notes in Theoretical Computer Science, 239, pages 73-83, Elsevier Science Publishers. 2009. [pdf] [bib]
Downloads:  pdf pdf (296 KB)  bib bib
Notes: The result was first presented at the workshop Infinity 2007. ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. In this paper we study complexity of the model-checking problem for probabilistic pushdown automata (pPDA) and qualitative fragments of two branching-time logics PCTL* and PECTL*. We prove that this problem is in 2-EXPTIME for pPDA and qualitative PCTL*. Consequently, we prove that model-checking of stateless pPDA (pBPA) and both qualitative PCTL* and qualitative PECTL* is 2-EXPTIME-hard. These results combined with results of several other papers give us that the model-checking problem for pPDA (and also for pBPA) and both qualitative PCTL* and qualitative PECTL* is 2-EXPTIME-complete. Finally, we survey known results on model-checking of pPDA and branching-time logics

QAV:

Home

People

Projects

Publications