BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking

  • Damien Bergamini
  • Nicolas Descoubes
  • Christophe Joubert
  • Radu Mateescu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


The equivalence checking problem consists in verifying that a system (e.g., a protocol) matches its abstract specification (e.g., a service) by comparing their Labeled Transition Systems (Ltss) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking: global verification requires to construct the two Ltss before comparison, whereas local (or on-the-fly) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.


Equivalence Relation Equivalence Check Label Transition System Alence Relation Modular Tool 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Andersen, H.R.: Model Checking and Boolean Graphs. Theoretical Computer Science 126(1), 3–30 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Cleaveland, R., Sokolsky, O.: Equivalence and Preorder Checking for Finite-State Systems. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 6, pp. 391–424. North-Holland, Amsterdam (2001)Google Scholar
  3. 3.
    Fernandez, J.-C., Mounier, L.: Verifying Bisimulations “On the Fly”. In: Quemada, J., Manas, J., Vázquez, E. (eds.) Proc. of FORTE 1990. North-Holland, Amsterdam (1990)Google Scholar
  4. 4.
    Fernandez, J.-C., Mounier, L.: A Tool Set for Deciding Behavioral Equivalences. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527. Springer, Heidelberg (1991)Google Scholar
  5. 5.
    Garavel, H.: OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. EASST Newsletter 4, 13–24 (2002): Also available as INRIA Report RT-0254 Google Scholar
  7. 7.
    Hermanns, H., Siegle, M.: Bisimulation Algorithms for Stochastic Process Algebras and their BDD-based Implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 244–265. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Joubert, C., Mateescu, R.: Distributed On-the-Fly Equivalence Checking. In: Brim, L., Leucker, M. (eds.) Proc. of PDMC 2004 (London, United Kingdom). ENTCS (September 2004) (to appear)Google Scholar
  9. 9.
    Mateescu, R.: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 81–96. Springer, Heidelberg (2003), Full version available as INRIA Research Report RR-4711 Google Scholar
  10. 10.

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Damien Bergamini
    • 1
  • Nicolas Descoubes
    • 1
  • Christophe Joubert
    • 1
  • Radu Mateescu
    • 1
  1. 1.Inria Rhône-Alpes/VasyMontbonnot St MartinFrance

Personalised recommendations