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

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

OBDRŽÁLEK Jan

Year of publication 2003
Type Article in Proceedings
Conference CAV 2003
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords parity games; mu-calculus; model-checking; tree-width
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.