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í: 2009
• Druh: Článek v odborném periodiku
• Časopis / Zdroj: Electronic Notes in Theoretical Computer Science
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://dx.doi.org/10.1016/j.entcs.2009.05.031
• 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