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 the of the algorithm may be software verification, since control flow graphs of programs written in high-level languages are usually of bounded tree-width. Finally, we discuss some implications and future work.
展开▼
