D 2003

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

OBDRŽÁLEK, Jan

Basic information

Original name

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

Authors

OBDRŽÁLEK, Jan (203 Czech Republic, guarantor)

Edition

Berlin Heidelberg, CAV 2003, p. 80-92, 13 pp. 2003

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/03:00008708

Organization unit

Faculty of Informatics

ISBN

3-540-40524-0

Keywords in English

parity games; mu-calculus; model-checking; tree-width

Tags

Changed: 26/5/2004 11:18, doc. Mgr. Jan Obdržálek, PhD.

Abstract

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.

Links

GA201/03/1161, research and development project
Name: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Verification of infinite-state systems
MSM 143300001, plan (intention)
Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing