| Identifikační kód | RIV/00216224:14330/14:00073430 |
|---|
| Název v anglickém jazyce | Branching-time model-checking of probabilistic pushdown automata |
|---|
| Druh | J - Článek v odborném periodiku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Tomáš Brázdil (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1762834)
Václav Brožek (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5532787)
Vojtěch Forejt (státní příslušnost: CZ - Česká republika, vedidk: 2477912)
Antonín Kučera (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9872655) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | Markov chains; pushdown automata |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1016/j.jcss.2013.07.001 |
|---|