Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems

Radu Mateescu
  • Fonction : Auteur
  • PersonId : 834239
Emilie Oudot
  • Fonction : Auteur
  • PersonId : 856675

Résumé

Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. Local (or on-the-fly) equivalence checking explores the synchronous product of the LTSs incrementally, allowing an efficient detection of errors in complex systems. In this paper, we consider the technique based on translating the equivalence checking problem in terms of the local resolution of a boolean equation system (BES). We propose two enhancements of this technique in the case of equivalent LTSs: a new, faster BES encoding of weak equivalence relations, and a new local BES resolution algorithm with a good average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and led to significant performance improvements.
Fichier principal
Vignette du fichier
Mateescu-Oudot-08-a.pdf (63.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00357770 , version 1 (01-02-2009)

Identifiants

Citer

Radu Mateescu, Emilie Oudot. Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems. MEMOCODE'2008, Jun 2008, Anaheim, United States. ⟨10.1109/MEMCOD.2008.4547690⟩. ⟨inria-00357770⟩
129 Consultations
158 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More