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