Fast Mu-calculus Model Checking when Tree-width is Bounded
| Authors | |
|---|---|
| Year of publication | 2003 |
| Type | Article in Proceedings |
| Conference | CAV 2003 |
| MU Faculty or unit | |
| 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: |