| BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERA. Branching-time model-checking of probabilistic pushdown automata. Journal of Computer and System Sciences. Academic Press, 2014, vol. 80, No 1, p. 139-156. ISSN 0022-0000. Available from: https://dx.doi.org/10.1016/j.jcss.2013.07.001. |
Other formats:
BibTeX
LaTeX
RIS
@article{1130512,
author = {Brázdil, Tomáš and Brožek, Václav and Forejt, Vojtěch and Kučera, Antonín},
article_number = {1},
doi = {http://dx.doi.org/10.1016/j.jcss.2013.07.001},
keywords = {Markov chains; pushdown automata},
language = {eng},
issn = {0022-0000},
journal = {Journal of Computer and System Sciences},
title = {Branching-time model-checking of probabilistic pushdown automata},
volume = {80},
year = {2014}
}
TY - JOUR
ID - 1130512
AU - Brázdil, Tomáš - Brožek, Václav - Forejt, Vojtěch - Kučera, Antonín
PY - 2014
TI - Branching-time model-checking of probabilistic pushdown automata
JF - Journal of Computer and System Sciences
VL - 80
IS - 1
SP - 139-156
EP - 139-156
PB - Academic Press
SN - 00220000
KW - Markov chains
KW - pushdown automata
N2 - In this paper we study the model-checking problem for probabilistic pushdown automata (pPDA) and branching-time probabilistic logics PCTL and PCTL*. We show that model-checking pPDA against general PCTL formulae is undecidable, but we yield positive decidability results for the qualitative fragments of PCTL and PCTL*. For these fragments, we also give a complete complexity classification.
ER -
BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERA. Branching-time model-checking of probabilistic pushdown automata. \textit{Journal of Computer and System Sciences}. Academic Press, 2014, vol.~80, No~1, p.~139-156. ISSN~0022-0000. Available from: https://dx.doi.org/10.1016/j.jcss.2013.07.001.
|
