. . "P(1M0545), P(GA201/03/1161), Z(MSM0021622419)" . "13"^^ . . "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."@en . . "On the Decidability of Temporal Properties of Probabilistic Pushdown Automata" . "14330" . . . . . . "[D5327A53DA61]" . "3"^^ . . "On the Decidability of Temporal Properties of Probabilistic Pushdown Automata"@en . . "3"^^ . "Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005)" . "RIV/00216224:14330/05:00012349!RIV10-GA0-14330___" . "Springer-Verlag" . "Stra\u017Eovsk\u00FD, Old\u0159ich" . "534455" . "February 24 - 26, 2005, Stuttgart, Germany" . "3-540-24998-2" . . "probabilistic pushdown automata; probabilistic temporal logics"@en . . "RIV/00216224:14330/05:00012349" . . . . "On the Decidability of Temporal Properties of Probabilistic Pushdown Automata" . . "Ku\u010Dera, Anton\u00EDn" . "Berlin" . . "On the Decidability of Temporal Properties of Probabilistic Pushdown Automata"@en . . . "Br\u00E1zdil, Tom\u00E1\u0161" . "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." . "2005-01-01+01:00"^^ .