Fast Mu-calculus Model Checking when Tree-width is Bounded
| Autoři | |
|---|---|
| Rok publikování | 2003 |
| Druh | Článek ve sborníku |
| Konference | CAV 2003 |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | parity games; mu-calculus; model-checking; tree-width |
| Popis | 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. |
| Související projekty: |