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

Jan Obdrzalek LFCS 4pm Tuesday 25 January 2003 Room 2511, JCMB, King's Buildings

I'll 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, I will discuss some implications and future work.