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