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...
| Autores principales: | , , |
|---|---|
| Formato: | Journal article |
| Lenguaje: | English |
| Publicado: |
2009
|