An Algebraic Framework for Abstract Model Checking | SpringerLink
Skip to main content
Springer Nature Link
Log in

An Algebraic Framework for Abstract Model Checking

  • Conference paper
  • First Online:
Abstraction, Reformulation, and Approximation (SARA 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2371))

  • 862 Accesses

Abstract

Symbolic forward analysis is a semi-algorithm that in many cases solves the model checking problem for infinite state systems in practice. This semi-algorithm is implemented in many practical model checking tools like UPPAAL [BLL+96], KRONOS [DT98] and HYTECH [HHWT97]. In most practical experiments, termination of symbolic forward analysis is achieved by employing abstractions resulting in an abstract symbolic forward analysis. This paper presents a unified algebraic framework for deriving and reasoning about abstract symbolic forward analysis procedures for a large class of infinite state systems with variables ranging over a numeric domain. The framework is obtained by lifting notions from classical algebraic theory of automata to constraints representing sets of states. Our framework provides sufficient conditions under which the derived abstract symbolic forward analysis procedure is always terminating or accurate or both. The class of infinite state systems that we consider here are (possibly non-linear) hybrid systems and (possibly non-linear) integer-valued systems. The central notions involved are those of constraint transformer monoids and coverings between constraint transformer monoids. We show concrete applications of our framework in deriving abstract symbolic forward analysis algorithms for timed automata and the two process bakery algorithm that are both terminating and accurate.

Support from the grants NSF award CCR99-70925, SRC award 99-TJ-688, and DARPA ITO Mobies award F33615-00-C-1707 is gratefully acknowledged

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems, 2000.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, LNCS 736, pages 209–229. Springer-Verlag, 1993.

    Google Scholar 

  3. P. Abdulla, K. Cerans, B. Jonsson, and T. K. Tsay. General decidability theorems for infinite state systems. In LICS, pages 313–321, 1996.

    Google Scholar 

  4. B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In O. Grumberg, editor, CAV’97: Computer Aided Verification, volume 1254 of LNCS, pages 167–178. Springer-Verlag, 1997.

    Google Scholar 

  5. Johan Bengtsson, Kim. G. Larsen, Fredrik Larsson, Paul Petersson, and Wang Yi. Uppaal in 1995. In T. Margaria and B. Steffen, editors, TACAS, LNCS 1055, pages 431–434. Springer-Verlag, 1996.

    Google Scholar 

  6. Bernard Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universite De Liege, Montefiore, Belgium, 1998.

    Google Scholar 

  7. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In the 4th ACM Symposium on Principles of Programming Languages, 1977.

    Google Scholar 

  8. P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6:69–95, 1998.

    Article  Google Scholar 

  9. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, CAV: Computer-Aided Verification, volume 1855 of LNCS, pages 154–169. Springer, 2000.

    Chapter  Google Scholar 

  10. R. Cleaveland, P. Iyer, and D. Yankelevich. Optimality in abstractions of model checking. In A. Mycroft, editor, SAS: Static Analysis Symposium, volume 983 of LNCS, pages 51–63. Springer, 1995.

    Google Scholar 

  11. H. Comon and Y. Jurski. Multiple Counters Automata, Safety Analysis, and Presburger Arithmetics. In Alan J. Hu and M. Y. Vardi, editors, CAV’98: Computer Aided Verification, volume 1427 of LNCS, pages 268–279. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  12. M. A. Colon and T. E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In A. Hu and M. Y. Vardi, editors, CAV: Computer-Aided Verification, volume 1427 of LNCS, pages 293–304. Springer, 1998.

    Chapter  Google Scholar 

  13. S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In N. Halbwachs and D. Peled, editors, CAV: Computer-Aided Verification, volume 1633 of LNCS, pages 160–171. Springer, 1999.

    Chapter  Google Scholar 

  14. G. Delzanno and A. Podelski. Model Checking in CLP. In R. Cleaveland, editor, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’99), volume 1579 of LNCS, pages 223–239. Springer-Verlag, March 1999.

    Chapter  Google Scholar 

  15. C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Bernhard Steffen, editor, TACAS98: Tools and Algorithms for the Construction of Systems, LNCS 1384, pages 313–329. Springer-Verlag, March/April 1998.

    Chapter  Google Scholar 

  16. S. Eilenberg. Automata, Languages and Machines, volume B. Academic Press, 1976.

    Google Scholar 

  17. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal of the Association of Computing Machinery (JACM), 47(2):361–413, March 2000.

    Google Scholar 

  18. S. Graf and H. Saidi. Construction of abstract state graphs with pvs. In O. Grumberg, editor, CAV: Computer-Aided Veri.cation, volume 1254 of LNCS, pages 72–83. Springer, 1997.

    Google Scholar 

  19. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. In O. Grumberg, editor, CAV97: Computer-aided Verification, LNCS 1254, pages 460–463. Springer-Verlag, 1997.

    Google Scholar 

  20. T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? In the 27th Annual Symposium on Theory of Computing, pages 373–382. ACM Press, 1995.

    Google Scholar 

  21. N. Halbwachs, Y-E. Proy, and P. Romanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.

    Article  Google Scholar 

  22. R. P. Kurshan and K. S. Namjoshi. Syntactic program transformations for automatic abstractions. In E. A. Emerson and A. P. Sistla, editors, CAV: Computer-Aided Verification, volume 1855 of LNCS, pages 435–449. Springer, 2000.

    Google Scholar 

  23. Y. Kesten, A. Pnueli, and M. Y. Vardi. Verification by augmented abstraction: The automata-theoretic view. In J. Flum and M. R. Artalejo, editors, CSL: Computer Science Logic, volume 1683 of LNCS, pages 141–156. Springer, 1999.

    Chapter  Google Scholar 

  24. K.G. Larsen, P. Pettersson, and W. Yi. Compositional and symbolic model checking of real-time systems. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 76–87. IEEE Computer Society Press, 1995.

    Google Scholar 

  25. G. Lafferriere, G. J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In F. W. Vaandrager and J. H. van Schuppen, editors, Hybrid Systems, Computation and Control, volume 1569 of LNCS, pages 137–151, 1999.

    Chapter  Google Scholar 

  26. S. Mukhopadhyay and A. Podelski. Beyond region graphs: Symbolic forward analysis of timed automata. In C. Pandurangan, V. Raman, and R. Ramanujam, editors, 19th International Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1738 of LNCS, pages 233–245, December 1999.

    Google Scholar 

  27. S. Mukhopadhyay and A. Podelski. Accurate widenings and boundedness properties, 2000.

    Google Scholar 

  28. S. Mukhopadhyay and A. Podelski. Compositional termination analysis of symbolic forward analysis for infinite state systems, 2000.

    Google Scholar 

  29. H. Saidi. Model checking guided abstraction and analysis. In J. Palsberg, editor, SAS: Static Analysis Symposium, LNCS. Springer, 2000.

    Google Scholar 

  30. H. Saidi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, CAV: Computer-Aided Verification, volume 1633 of LNCS, pages 455–469. Springer, 1999.

    Google Scholar 

  31. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. In O. Grumberg, editor, CAV97: Computer-aided Verification, LNCS 1254, pages 460–463. Springer-Verlag, 1997.

    Google Scholar 

  32. T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? In the 27th Annual Symposium on Theory of Computing, pages 373–382. ACM Press, 1995.

    Google Scholar 

  33. N. Halbwachs, Y-E. Proy, and P. Romanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.

    Article  Google Scholar 

  34. R. P. Kurshan and K. S. Namjoshi. Syntactic program transformations for automatic abstractions. In E. A. Emerson and A. P. Sistla, editors, CAV: Computer-Aided Verification, volume 1855 of LNCS, pages 435–449. Springer, 2000.

    Google Scholar 

  35. Y. Kesten, A. Pnueli, and M. Y. Vardi. Verification by augmented abstraction: The automata-theoretic view. In J. Flum and M. R. Artalejo, editors, CSL: Computer Science Logic, volume 1683 of LNCS, pages 141–156. Springer, 1999.

    Chapter  Google Scholar 

  36. K.G. Larsen, P. Pettersson, and W. Yi. Compositional and symbolic model checking of real-time systems. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 76–87. IEEE Computer Society Press, 1995.

    Google Scholar 

  37. G. Lafferriere, G. J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In F. W. Vaandrager and J. H. van Schuppen, editors, Hybrid Systems, Computation and Control, volume 1569 of LNCS, pages 137–151, 1999.

    Chapter  Google Scholar 

  38. S. Mukhopadhyay and A. Podelski. Beyond region graphs: Symbolic forward analysis of timed automata. In C. Pandurangan, V. Raman, and R. Ramanujam, editors, 19th International Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1738 of LNCS, pages 233–245, December 1999.

    Google Scholar 

  39. S. Mukhopadhyay and A. Podelski. Accurate widenings and boundedness properties, 2000.

    Google Scholar 

  40. S. Mukhopadhyay and A. Podelski. Compositional termination analysis of symbolic forward analysis for infinite state systems, 2000.

    Google Scholar 

  41. H. Saidi. Model checking guided abstraction and analysis. In J. Palsberg, editor, SAS: Static Analysis Symposium, LNCS. Springer, 2000.

    Google Scholar 

  42. H. Saidi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, CAV: Computer-Aided Verification, volume 1633 of LNCS, pages 455–469. Springer, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, 66123, Saarbrücken, Germany

    Supratik Mukhopadhyay & Andreas Podelski

Authors
  1. Supratik Mukhopadhyay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Podelski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. College of Computing, Georgia Institute of Technology, 801 Atlantic Dr NW, Atlanta, GA, 30332-0280, USA

    Sven Koenig

  2. Department of Computing Science, Universtity of Alberta, 2-21 Athabasca Hall, Edmonton, Alberta, T6G 2E8, Canada

    Robert C. Holte

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mukhopadhyay, S., Podelski, A. (2002). An Algebraic Framework for Abstract Model Checking. In: Koenig, S., Holte, R.C. (eds) Abstraction, Reformulation, and Approximation. SARA 2002. Lecture Notes in Computer Science(), vol 2371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45622-8_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-45622-8_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43941-7

  • Online ISBN: 978-3-540-45622-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation