Branching-Time Model-Checking of Probabilistic Pushdown Automata

• Název česky: Ověřování modelu pro logiky větvícího se času nad pravděpodobnostními zásobníkovými automaty
• Autoři: BRÁZDIL Tomáš; BROŽEK Václav; FOREJT Vojtěch
• Rok publikování: 2007
• Druh: Článek ve sborníku
• Konference: Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: model-checking; Markov chains; temporal logics; probabilistic pushdown automata
• Popis: Byla dosažena úplná klasifikace výpočetní složitosti problému ověření modelu pro pravděpodobnostní zásobníkové automaty a kvalitativní fragmenty logik PCTL, PCTL* a PECTL*.

Související projekty

• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy