A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2003

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

Résumé

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.
Fichier principal
Vignette du fichier
RR-4711.pdf (234.24 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00071875 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00071875 , version 1

Citer

Radu Mateescu. A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. RR-4711, INRIA. 2003. ⟨inria-00071875⟩
102 Consultations
207 Téléchargements

Partager

Gmail Facebook X LinkedIn More