Skip to main content
SpringerLink
Log in

Beyond Regular Model Checking

Extended Abstract

  • Conference paper
  • First Online:
FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001)

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

Abstract

In recent years, it has been established that regular model checking can be successfully applied to several parameterized verification problems. However, there are many parameterized verification problems that cannot be described by regular languages, and thus cannot be verified using regular model checking. In this study we try to practice symbolic model checking using classes of languages more expressive than the regular languages. We provide three methods for the uniform verification of non-regular parameterized systems.

This work was supported in part by the European Commission (FET project ADVANCE, contract No IST-1999-29082), and carried out at the John von Neumann Minerva Center for the Verification of Reactive Systems.

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. P.A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. CAV’98, LNCS, volume 1427, p. 305–318. Springer-Verlag, 1998.

    Google Scholar 

  2. P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. CAV’99, volume 1633 of LNCS, p. 134 Springer-Verlag, 1999.

    Google Scholar 

  3. K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.

    Google Scholar 

  4. J-P. Bodeveix and M. Filali. Experimenting acceleration methods for the validation of infinite state systems. In DSVV’2000, Taipei, Taiwan, April 2000.

    Google Scholar 

  5. B. Boigelot and P. Godefroid. Symbolic verification of coomunication protocols with infinite state spaces using QDDs. CAV’96, volume 1102 of LNCS, p. 1–12. Springer-Verlag, 1996.

    Google Scholar 

  6. B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. of the Fourth International Static Analysis Symposium, LNCS Springer-Verlag, 1997.

    Google Scholar 

  7. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. CONCUR’97, LNCS, volume 1243, p. 135. Springer-Verlag, 1997.

    Google Scholar 

  8. A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO-channel systems with non-regular sets of configurations. In ICALP’97, volume 1256 of LNCS Springer-Verlag, 1997.

    Google Scholar 

  9. A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touilli. Regular model checking. CAV’00, volume 1855 of LNCS, p. 403–418. Springer-Verlag, 2000.

    Google Scholar 

  10. A. Bouajjani and O. Maler. Reachability analysis of push-down automata. In Workshop on Infinite-state Systems, Pisa, 1996.

    Google Scholar 

  11. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  12. O. Burkat and B. Steffen. Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89–125, 1995.

    MathSciNet  Google Scholar 

  13. E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR’95, p. 395–407, Philadelphia, PA, August 1995.

    Google Scholar 

  14. H. Comon and Y. Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In CAV’98, LNCS, p. 268–279, 1998.

    Google Scholar 

  15. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL’97.

    Google Scholar 

  16. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. CAV’00, volume 1855 of LNCS, p. 232–247. Springer-Verlag, 2000.

    Google Scholar 

  17. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Proc. Infinity’97, Electronic Notes in Theoretical Computer Science, 1997.

    Google Scholar 

  18. L. Fribourg and H. Olsen. Reachability sets of parametrized rings as regular languages. In Proc. Infinity’97, Electronic Notes in Theoretical Computer Science, volume 9, July 1997.

    Google Scholar 

  19. J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts, 1979.

    MATH  Google Scholar 

  20. B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In S. Graf, editor, Proceedings of TACAS’00, LNCS, 2000. To Appear.

    Google Scholar 

  21. Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. CAV’97, LNCS, p. 424–435. Springer-Verlag, 1997.

    Google Scholar 

  22. D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL’97, Paris, 1997.

    Google Scholar 

  23. G.L. Peterson. Myths about the mutual exclusion problem. Info. Proc. Lett., 12(3):115, 1981.

    Google Scholar 

  24. A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. CAV’00, volume 1855 of LNCS, p. 328–343. Springer-Verlag, 2000.

    Google Scholar 

  25. G. Ricart and A.K. Agrawala. An optimal algorithm for mutual exclusion in computer networks. Comm. ACM, 24(1):9–17, 1981. Corr. ibid. 1981, p.581.

    Article  MathSciNet  Google Scholar 

  26. G. Senizergues. The equivalence problem for deterministic pushdown automata is decidable. volume 1256 of LNCS, p. 671–681, 1997.

    Google Scholar 

  27. E. Shahar. The tlv system and its application. Master’s thesis,Weizmann Institute, 1996.

    Google Scholar 

  28. Colin Stirling. Decidability of dpda equivalence. FODDACS’01, LNCS Springer-Verlag, 2001.

    Google Scholar 

  29. P. Wolper and B. Boigelot. Symbolic verification with periodic sets. In D. Dill, editor, CAV’94, volume 818 of LNCS, p. 55–67. Springer-Verlag, 1994.

    Google Scholar 

  30. Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. CAV’98, LNCS, volume 1427, p. 88–97. Springer-Verlag, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept of Computer Science, The Weizmann Institute of Science, Rehovot, Israel

    Dana Fisman & Amir Pnueli

Authors
  1. Dana Fisman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, 560012, Bangalore, India

    Ramesh Hariharan  & V. Vinay  & 

  2. Chennai Mathematical Institute, 92 G.N. Chetty Road, 600 017, Chennai, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fisman, D., Pnueli, A. (2001). Beyond Regular Model Checking. In: Hariharan, R., Vinay, V., Mukund, M. (eds) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2001. Lecture Notes in Computer Science, vol 2245. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45294-X_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45294-X_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43002-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation