Techniques for Solving Boolean Equation Systems

Reference:

Misa Keinänen. Techniques for solving boolean equation systems. Research Report A105, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, November 2006. Doctoral dissertation.

Abstract:

Boolean equation systems are ordered sequences of Boolean equations decorated with least and greatest fixpoint operators. Boolean equation systems provide a useful framework for formal verification because various specification and verification problems, for instance, -calculus model checking can be represented as the problem of solving Boolean equation systems. The general problem of solving a Boolean equation system is a computationally hard task, and no polynomial time solution technique for the problem has been discovered so far. In this thesis, techniques for finding solutions to Boolean equation systems are studied and new methods for solving such systems are devised.

The thesis presents a general framework that allows for dividing Boolean equation systems into individual blocks and solving these blocks in isolation with special techniques. Three special techniques are presented, namely: (i) new specialized algorithms for disjunctive and conjunctive form Boolean equation systems, (ii) a new encoding of a general form Boolean equation system into answer set programming, and (iii) new encodings of a general form Boolean equation systems into satisfiability problems. The approaches (ii) and (iii) are motivated by the recent success of answer set programming solvers and satisfiability solvers in formal verification.

First, the thesis presents especially fast solution algorithms for disjunctive and conjunctive classes of Boolean equation systems. These special algorithms are useful because many practically relevant model checking problems can be represented as Boolean equation systems that are disjunctive or conjunctive. The new algorithms have been implemented and the performance of the algorithms has been compared experimentally on communication protocol verification examples.

Second, the thesis gives a translation of the problem of solving a general form Boolean equation system into the problem of finding a stable model of a logic program. The translation allows to use implementations of answer set programming solvers to solve Boolean equation systems. Experimental tests have been performed using the presented approach and these experiments indicate the usefulness of answer set programming in this problem domain.

Third, the thesis presents reductions from the problem of solving general form Boolean equation systems to the satisfiability problems of difference logic and propositional logic. The reductions allow to use implementations of satisfiability solvers to solve Boolean equation systems. The presented reductions have been implemented and it is shown via experiments that the new approach leads to practically efficient methods to solve general Boolean equation systems.

Keywords:

answer set programming, Boolean equation systems, computer-aided verification, satisfiability problems

Suggested BibTeX entry:

@techreport{HUT-TCS-A105,
    address = {Espoo, Finland},
    author = {Misa Kein\"anen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {November},
    note = {Doctoral dissertation},
    number = {A105},
    pages = {xii+95},
    title = {Techniques for Solving Boolean Equation Systems},
    type = {Research Report},
    year = {2006},
}