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.
|
