Detailed Information on Publication Record
2014
Branching-time model-checking of probabilistic pushdown automata
BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERABasic information
Original name
Branching-time model-checking of probabilistic pushdown automata
Authors
BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Václav BROŽEK (203 Czech Republic, belonging to the institution), Vojtěch FOREJT (203 Czech Republic) and Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution)
Edition
Journal of Computer and System Sciences, Academic Press, 2014, 0022-0000
Other information
Language
English
Type of outcome
Článek v odborném periodiku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Netherlands
Confidentiality degree
není předmětem státního či obchodního tajemství
Impact factor
Impact factor: 1.138
RIV identification code
RIV/00216224:14330/14:00073430
Organization unit
Faculty of Informatics
UT WoS
000325386500011
Keywords (in Czech)
Markovské procesy; zásobníkové automaty
Keywords in English
Markov chains; pushdown automata
Tags
Tags
International impact, Reviewed
Změněno: 27/4/2015 03:17, RNDr. Pavel Šmerk, Ph.D.
Abstract
V originále
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.
Links
| GAP202/10/1469, research and development project |
|