Model Checking Probabilistic Pushdown Automata

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Ověřování formulí temporálních logik pro pravděpodobnostní zásobníkové automaty
Autoři

ESPARZA Javier KUČERA Antonín MAYR Richard

Rok publikování 2006
Druh Článek v odborném periodiku
Časopis / Zdroj Logical Methods in Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www LMCS home page
Obor Informatika
Klíčová slova pushdown automata; Markov chains; probabilistic model checking
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.