Fast Mu-Calculus Model Checking when Tree-Width Is Bounded

We show that the model checking problem for µ-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. 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. The given algorithm is then modified to obtain a new algorithm for µ-calculus model checking. One possible use of this algorithm may be software verification, since control flow graphs of programs written in high-level languages are usually of bounded treewidth. Finally, we discuss some implications and future work.

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Jan Obdrzálek
• Keywords: CAV 2003, Formal Methods, Model Checking, Model Checking Problem, µ-calculus Model Checking