Informační systém MU
OBDRŽÁLEK, Jan. Fast Mu-calculus Model Checking when Tree-width is Bounded. In CAV 2003. Berlin Heidelberg: Springer-Verlag, 2003. s. 80-92, 13 s. ISBN 3-540-40524-0.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Fast Mu-calculus Model Checking when Tree-width is Bounded
Autoři OBDRŽÁLEK, Jan (203 Česko, garant).
Vydání Berlin Heidelberg, CAV 2003, od s. 80-92, 13 s. 2003.
Nakladatel Springer-Verlag
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/03:00008708
Organizační jednotka Fakulta informatiky
ISBN 3-540-40524-0
Klíčová slova anglicky parity games; mu-calculus; model-checking; tree-width
Štítky Model-Checking, mu-calculus, parity games, tree-width
Změnil Změnil: doc. Mgr. Jan Obdržálek, PhD., učo 1552. Změněno: 26. 5. 2004 11:18.
Anotace
We show that the model checking problem for mu-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. Since control flow graphs of programs written in high-level languages are usually of bounded tree-width, this gives us a faster algorithm for software model checking. The result is presented by first showing a related result: the winner in a parity game on a graph of bounded tree-width can be decided in polynomial time. Modification of this algorithm gives us a completely new algorithm for mu-calculus model checking. Finally, we discuss some implications and future work.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
Zobrazeno: 3. 8. 2020 16:58