Model Checking Probabilistic Pushdown Automata

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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:	Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy