Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{563891, author = {Brázdil, Tomáš and Kučera, Antonín and Stražovský, Oldřich}, address = {Berlin}, booktitle = {Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005)}, keywords = {probabilistic pushdown automata; probabilistic temporal logics}, language = {eng}, location = {Berlin}, isbn = {3-540-24998-2}, pages = {145-157}, publisher = {Springer}, title = {On the Decidability of Temporal Properties of Probabilistic Pushdown Automata}, year = {2005} }
TY - JOUR ID - 563891 AU - Brázdil, Tomáš - Kučera, Antonín - Stražovský, Oldřich PY - 2005 TI - On the Decidability of Temporal Properties of Probabilistic Pushdown Automata PB - Springer CY - Berlin SN - 3540249982 KW - probabilistic pushdown automata KW - probabilistic temporal logics N2 - 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. ER -
BRÁZDIL, Tomáš, Antonín KUČERA a Oldřich STRAŽOVSKÝ. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. V. Diekert, B. Durand (Eds.). In \textit{Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005)}. Berlin: Springer. s.~145-157. ISBN~3-540-24998-2. 2005.
|