2003 | OriginalPaper | Buchkapitel
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded
verfasst von : Jan Obdržálek
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 tree-width. Finally, we discuss some implications and future work.