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; 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
• 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