J 2006

Model Checking Probabilistic Pushdown Automata

ESPARZA, Javier; Antonín KUČERA a Richard MAYR

Základní údaje

Originální název

Model Checking Probabilistic Pushdown Automata

Název česky

Ověřování formulí temporálních logik pro pravděpodobnostní zásobníkové automaty

Autoři

ESPARZA, Javier (724 Španělsko); Antonín KUČERA (203 Česká republika, garant) a Richard MAYR (276 Německo)

Vydání

Logical Methods in Computer Science, 2006, 1860-5974

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/06:00016670

Organizační jednotka

Fakulta informatiky

UT WoS

000223180900002

Klíčová slova anglicky

pushdown automata; Markov chains; probabilistic model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 17:26, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

ORIG CZ

V originále

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for PCTL and the subclass of stateless pPDA. Finally, we consider the class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.

Česky

V článku se zkoumá problém algoritmické ověřitelnosti dané formule temporální logiky pro daný pravděpodobnostní zásobníkový automat. Nejprve jsou vyšetřeny formule, které lze specifikovat jako parametrizovanou náhodnou procházku. Pak jsou vyšetřeny obecnější formule definovatelné v logice PCTL a jejím kvalitativním fragmentu.

Návaznosti

MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky