Fast Mu-calculus Model Checking when Tree-width is Bounded

OBDRŽÁLEK, Jan. Fast Mu-calculus Model Checking when Tree-width is Bounded. In CAV 2003. Berlin Heidelberg: Springer-Verlag, 2003, s. 80-92. ISBN 3-540-40524-0.

Základní údaje

Originální název

Fast Mu-calculus Model Checking when Tree-width is Bounded

Autoři

OBDRŽÁLEK, Jan

Vydání

Berlin Heidelberg, CAV 2003, od s. 80-92, 13 s. 2003

Nakladatel

Springer-Verlag

---

Další údaje

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í

Označené pro přenos do RIV

Ano

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

---

Anotace

V originále

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 VaV	Název: Verifikace nekonečně stavových systémů Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM 143300001, záměr	Ná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, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů