A generic on-the-fly solver for alternation-free boolean equation systems

Abstract

Boolean Equation Systems (BESs) offer a useful representation for various verification problems on finite-state concurrent systems, such as equivalence/preorder checking and model checking. In particular, on-the-fly resolution methods enable a demand-driven construction of the BES (and hence, of the state space) during verification. In this paper, we present a generic library dedicated to on-the-fly resolution of alternation-free BESS. Four resolution algorithms are currently provided by the library: A1, A2 are general, the latter being optimized to produce small-depth diagnostics, and A3, A4 are specialized for handling acyclic and disjunctive/conjunctive BESS in a memory-efficient way. The library is developed within the CADP toolbox and serves as engine for on-the-fly equivalence/preorder checking modulo five widely-used relations, and for model checking of alternation-free μ-calculus. © Springer-Verlag Berlin Heidelberg 2003.