On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš KUČERA Antonín STRAŽOVSKÝ Oldřich

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.