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í platnosti formulí temporálních logik pro procesy zásobníkových automatů
Autoři	ESPARZA Javier KUČERA Antonín MAYR Richard
Rok publikování	2004
Druh	Článek ve sborníku
Konference	Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	Probabilistic Pushdown Automata; Model Checking
Popis	V práci je rozebrána problematika automatického ověřování platnosti formulí temporálních logik pro procesy pravděpodobnostních zásobníkových automatů. Nejprve je uvažována třída vlastností, která je formulovatelná jako zobecněný problém náhodné procházky. Je dokázáno, že kvalitativní i kvantitativní varianta tohoto problému je rozhodnutelná. Pak je dokázána rozhodnutelnost problému platnosti dané formule kvalitativního fragmentu logiky PCTL pro daný zásobníkový proces. Jsou také uvažovány vlastnosti popsatelné pomocí deterministických Buchiho automatů a ukázána rozhodnutelnost příslušných problémů.
Související projekty:	Verifikace nekonečně stavových systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů