SOLVING BOOLEAN EQUATION SYSTEMS

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 work, 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 answe