Solving Boolean Equation Systems

Reference:

Misa Keinänen. Solving boolean equation systems. Research Report A99, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, November 2005.

Abstract:

Boolean equation systems are ordered sequences of Boolean equations decorated with fixpoint operators. Boolean equation systems provide a useful framework for computer aided verification because various specification and verification problems can be encoded as the problem of solving such fixpoint equation systems. In this thesis, techniques for finding solutions to Boolean equation systems are studied, and new methods for solving such systems are devised. An approach to solve a general form Boolean equation system, which simplifies the process of finding the solution by dividing the system into more simple subsystems and solving these by optimized procedures, is introduced and analyzed. New solution algorithms for disjunctive and conjunctive classes of Boolean equation systems are presented, together with an implementation and experimental evaluation of a solver for these classes. A novel translation of the problem of solving a general form Boolean equation system into the problem of finding a stable model of a logic program is given. The translation allows to use an implementation of an answer set programming framework, the Smodels system, to solve Boolean equation systems. Experimental tests have been performed using the presented approach and these experiments indicate the effectiveness of using answer set programming in this problem domain.

Keywords:

Boolean equation systems, computer aided verification, model checking, logic programs, stable model semantics

Suggested BibTeX entry:

@techreport{HUT-TCS-A99,
    address = {Espoo, Finland},
    author = {Misa Kein\"anen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {November},
    number = {A99},
    pages = {52},
    title = {Solving Boolean Equation Systems},
    type = {Research Report},
    year = {2005},
}