Branching-Time Model-Checking of Probabilistic Pushdown Automata.
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 tha this problem is in 2-EXPTIME for pPDA and qualitative PCTL*. Consequently, we prove that model-checking of...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2009
|