Modal μ-calculus, model checking and Gauβ elimination

Abstract

In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gaufl elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal μ-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.