On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Proceedings |
| Conference | Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | probabilistic pushdown automata; probabilistic temporal logics |
| Description | We consider qualitative and quantitative model-checking problems for probabilistic pushdown automata (pPDA) and various temporal logics. We prove that the qualitative and quantitative model-checking problem for omega-regular properties and pPDA is in 2-EXPSPACE and 3-EXPTIME, respectively. We also prove that model-checking the qualitative fragment of the logic PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative fragment of PCTL for pPDA is in EXPSPACE. Furthermore, model-checking the qualitative fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA. Finally, we show that PCTL model-checking is undecidable for pPDA, and PCTL+ model-checking is undecidable even for stateless pPDA. |
| Related projects: |