CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems

Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Boolean Equation Systems (BESs) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. 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 BES. In this report, we present a generic software library dedicated to on-the-fly resolution of alternation-free BESs (i.e., without mutually recursive minimal and maximal fixed point equations). Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive BESs in a memory-efficient way. The library is developed within the CADP verification toolbox using the generic OPEN/CAESAR environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely-used equivalence relations, on-the-fly model checking of regular alternation-free mu-calculus, and on-the-fly reduction of state spaces based on tau-confluence.
Type de document :
[Research Report] RR-5948, INRIA. 2006, pp.38
Liste complète des métadonnées

Littérature citée [55 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 18 juillet 2006 - 11:12:21
Dernière modification le : mercredi 11 avril 2018 - 01:55:46
Document(s) archivé(s) le : lundi 20 septembre 2010 - 15:54:39



  • HAL Id : inria-00084628, version 2



Radu Mateescu. CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. [Research Report] RR-5948, INRIA. 2006, pp.38. 〈inria-00084628v2〉



Consultations de la notice


Téléchargements de fichiers