Bisimulation and Model Checking

  • Kathi Fisler
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


State space minimization techniques are crucial for combating state explosion. A variety of verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. This paper explores the third use in the context of verifying invariant properties. We consider three bisimulation minimization algorithms. From each, we produce an on-the-fly model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, lead us to conclude that bisimulation minimization does not appear to be viable in the context of invariance verification because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.


  1. 1.
    Bouajjani, A., J.C. Fernandez and N. Halbwachs. Minimal model generation. In Proc. Intl. Conference on Computer-Aided Verification (CAV), pages 197–203. Springer-Verlag, 1990.Google Scholar
  2. 2.
    Fisler, K. and M. Y. Vardi. Bisimulation minimization in an automata-theoretic verification framework. In Proc. Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 115–132. Springer-Verlag, 1998.Google Scholar
  3. 3.
    Fisler, K. and M.Y. Vardi. Bisimulation and model checking (extended version). Technical report TR99-339, Rice University, Department of Computer Science, 1999. Available at
  4. 4.
    Hennessy, M. and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of ACM, 32:137–161, 1985.zbMATHCrossRefGoogle Scholar
  5. 5.
    Lee, D. and M. Yannakakis. Online minimization of transition systems. In Proc. 24th ACM Symposium on Theory of Computing, pages 264–274, Victoria, May 1992.Google Scholar
  6. 6.
    Milner, R. A Calculus of Communicating Systems. Springer Verlag, Berlin, 1980.zbMATHGoogle Scholar
  7. 7.
    Paige, R. and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16:973–989, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    The VIS Group. VIS: A system for verification and synthesis. In Proc. of the 8th Intl. Conference on Computer Aided Verification (CAV), pages 428–432. Springer Verlag, July 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Kathi Fisler
    • 1
  • Moshe Y. Vardi
    • 1
  1. 1.Department of Computer ScienceRice UniversityTXUSA

Personalised recommendations