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 Gauß 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.
|Number of pages||17|
|Publication status||Published - May 1995|
|Event||1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995 - Aarhus, Denmark|
Duration: 19 May 1995 → 20 May 1995
Conference number: 1
|Workshop||1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995|
|Period||19/05/95 → 20/05/95|