Skip to main content
SpringerLink
Log in

Bisimulation Minimization in an Automata-Theoretic Verification Framework

  • Conference paper
  • First Online:
Formal Methods in Computer-Aided Design (FMCAD 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1522))

Included in the following conference series:

Abstract

Bisimulation is a seemingly attractive state-space minimization technique because it can be computed automatically and yields the smallest model preserving all µcalculus formulas. It is considered impractical for symbolic model checking, however, because the required BDDs are prohibitively large for most designs. We revisit bisimulation minimization, this time in an automata-theoretic framework. Bisimulation has potential in this framework because after intersecting the design with the negation of the property, minimization can ignore most of the atomic propositions. We compute bisimulation using an algorithm due to Lee and Yannakakis that represents bisimulation relations by their equivalence classes and only explores reachable classes. This greatly improves on the time and memory usage of naÏve algorithms.We demonstrate that bisimulation is practical for many designs within the automata-theoretic framework. In most cases, however, the cost of performing this reduction still outweighs that of conventional model checking.

Supported in part by NSF grants CDA-9625898, CCR-9628400 and CCR-9700061, and by a grant from the Intel Corporation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of the IEEE Real-Time Systems Symposium, pages 157–166, 1992.

    Google Scholar 

  2. A. Aziz, V. Singhal, G.M. Swamy, and R.K. Brayton. Minimizing interacting finite state machines: A compositional approach to language containment. In Proc. of the International Conference on Computer Design (ICCD), 1994.

    Google Scholar 

  3. R. I. Bahar et al. Algebraic decision diagrams and their applications. In Proc. of the International Conference on Computer-Aided Design, pages 188–191, 1993.

    Google Scholar 

  4. I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Conference on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 182–193, Stanford, June1994.

    Google Scholar 

  5. A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247–269, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  6. A. Bouali. XEVE, an ESTEREL verification environment. In Proc. of the International Conference on Computer-Aided Verification (CAV), pages 500–504, 1998.

    Google Scholar 

  7. A. Bouali and R. de Simone. Symbolic bisimulation minimization. In Proc. of the International Conference on Computer-Aided Verification (CAV), pages 96–108, 1992.

    Google Scholar 

  8. Y. Choueka. Theories of automata on Ω-tapes: A simplified approach. Journal of Computer and System Sciences, 8:117–141, 1974.

    Article  MATH  MathSciNet  Google Scholar 

  9. E.M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design, 9(1/2):77–104, August 1996.

    Google Scholar 

  10. E.M. Clarke, O. Grumberg, and D.E. Long. Model-checking and abstraction. In Proc. of the 19th ACM Symposium on Principles of Programming Languages, pages 343–354, 1992.

    Google Scholar 

  11. E.M. Clarke and R.P. Kurshan. Computer aided verification. IEEE Spectrum, 33:61–67, 1986.

    Article  Google Scholar 

  12. C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.

    Article  Google Scholar 

  13. The CUDD package. Available from http://vlsi.colorado.edu/~fabio/.

  14. D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Technische Universiteit Eindhoven, 1996.

    Google Scholar 

  15. D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In Proc. 5th Int.l Conference on Computer-Aided Verification, pages 479–490, 1993.

    Google Scholar 

  16. D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(2), March 1997.

    Google Scholar 

  17. K. Fisler and M.Y. Vardi. Bisimulation minimization in an automata-theoretic verification framework (extended version). Technical report, Rice University, Department of Computer Science, 1998.

    Google Scholar 

  18. J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. of the International Conference on Automata, Languages, and Programming, pages 626–638, 1990.

    Google Scholar 

  19. The VIS Group. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, In the Proc. of the 8th International Conference on Computer Aided Verification, pages 428–432. Springer Verlag, July 1996.

    Google Scholar 

  20. O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843–871, 1994.

    Article  Google Scholar 

  21. V. Gyuris and A. P. Sistla. On-the-fly model checking under fairness that exploits symmetry. In Proc. of International Conference on Computer-Aided Verification (CAV), pages 232–243, 1997.

    Google Scholar 

  22. R. Hardin, R.P. Kurshan, S. Shukla, and M.Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. of the International Conference on Computer-Aided Verification, 1997.

    Google Scholar 

  23. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of ACM, 32:137–161, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  24. T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. 8th Conference on Concurrency Theory, volume 1243 of Lecture Notes in Computer Science, pages 273–287, Warsaw, July 1997. Springer-Verlag.

    Google Scholar 

  25. C. N. Ip and D. L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1/2):41–76, August 1996.

    Google Scholar 

  26. A. Kick. Formula dependent model reduction through elimination of invisible transitions for checking fragments of CTL. Technical Report 1995–27, UniversitÄt Karlsruhe, 1995.

    Google Scholar 

  27. O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conference on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 408–422, August 1995. Springer-Verlag.

    Google Scholar 

  28. R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.

    Google Scholar 

  29. D. Lee and M. Yannakakis. Online minimization of transition systems. In Proc. 24th ACM Symposium on Theory of Computing, pages 264–274, May 1992.

    Google Scholar 

  30. David E. Long. Model-checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, 1993.

    Google Scholar 

  31. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, Berlin, 1980.

    MATH  Google Scholar 

  32. S. Minato. Binary decision diagrams and applications for VLSI CAD. Kluwer Academic Publishers, 1996.

    Google Scholar 

  33. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.

    Google Scholar 

  34. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming, pages 184–192, St. Petersburgh, January 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Rice University, 6100 S. Main, MS 132, Houston, TX 77005-1892, USA

    Kathi Fisler & Moshe Y. Vardi

Authors
  1. Kathi Fisler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Utah, 50 S Central Campus, Salt Lake City, UT, 841112-9205, USA

    Ganesh Gopalakrishnan

  2. Department of Computer Science, Brigham Young University, 3361 TMCB, Provo, UT, 84602-6576, USA

    Phillip Windley

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fisler, K., Vardi, M.Y. (1998). Bisimulation Minimization in an Automata-Theoretic Verification Framework. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-49519-3_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65191-8

  • Online ISBN: 978-3-540-49519-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation