A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems

Boolean Equation Systems are a useful formalism for modeling various verification problems of finite-state concurrent systems, in particular the equivalence checking and the model checking problems. These problems can be solved on-the-fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding boolean equation system. In this report, we present a generic software library dedicated to on-the-fly resolution of alternation-free boolean equation systems. Four resolution algorithms are currently provided by the library: A1 and A2 are general algorithms, the latter being optimized to produce small-depth diagnostics, whereas A3 and A4 are specialized algorithms for handling acyclic and disjunctive/conjunctive boolean equation systems in a memory-efficient way. The library is developed within the Cadp verification toolbox and is used for both on-the-fly equivalence checking (five widely-used equivalence relations are supported) and for on-the-fly model checking of alternation-free modal mu-calculus