Improved On-the-Fly Equivalence Checking using Boolean Equation Systems

Radu Mateescu 1 Emilie Oudot 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Equivalence checking is a classical verification method for ensuring the compatibility of a finite-state concurrent system (protocol) with its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. The local (or on-the-fly) approach for equivalence checking combats state explosion by exploring the synchronous product of the LTSs incrementally, thus allowing an efficient detection of errors in complex systems. However, when the two LTSs being compared are equivalent, the on-the-fly approach is outperformed by the global one, which completely builds the LTSs and computes the equivalence classes between states using partition refinement. In this paper, we consider the approach based on translating the on-the-fly equivalence checking problem in terms of the local resolution of a boolean equation system (BES). We propose two enhancements of the approach in the case of equivalent LTSs: a new, faster encoding of equivalence relations in terms of BESs, and a new local BES resolution algorithm with a better average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and they led to significant performance improvements w.r.t. existing on-the-fly equivalence checking algorithms.
Type de document :
Rapport
[Research Report] RR-6777, INRIA. 2008, pp.31
Liste complète des métadonnées

Littérature citée [47 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00347627
Contributeur : Radu Mateescu <>
Soumis le : mardi 16 décembre 2008 - 12:56:36
Dernière modification le : mercredi 11 avril 2018 - 01:54:41
Document(s) archivé(s) le : mardi 8 juin 2010 - 17:22:16

Fichier

RR-6777.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00347627, version 1

Collections

Citation

Radu Mateescu, Emilie Oudot. Improved On-the-Fly Equivalence Checking using Boolean Equation Systems. [Research Report] RR-6777, INRIA. 2008, pp.31. 〈inria-00347627〉

Partager

Métriques

Consultations de la notice

269

Téléchargements de fichiers

106