J 2014

Branching-time model-checking of probabilistic pushdown automata

BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT a Antonín KUČERA

Základní údaje

Originální název

Branching-time model-checking of probabilistic pushdown automata

Autoři

BRÁZDIL, Tomáš (203 Česká republika, domácí), Václav BROŽEK (203 Česká republika, domácí), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant, domácí)

Vydání

Journal of Computer and System Sciences, Academic Press, 2014, 0022-0000

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 1.138

Kód RIV

RIV/00216224:14330/14:00073430

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000325386500011

Klíčová slova česky

Markovské procesy; zásobníkové automaty

Klíčová slova anglicky

Markov chains; pushdown automata

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 27. 4. 2015 03:17, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GAP202/10/1469, projekt VaV
Název: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů