Techniques for solving Boolean equation systems
Misa Keinänen · Aaltodoc (Aalto University) · 2006
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: