Beyond Regular Model Checking

Extended Abstract
  • Dana Fisman
  • Amir Pnueli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


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.


Model Check Regular Expression Symbolic Representation Mutual Exclusion Regular Language 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 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. 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. 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. 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. 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. 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. 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. 10.
    A. Bouajjani and O. Maler. Reachability analysis of push-down automata. In Workshop on Infinite-state Systems, Pisa, 1996.Google Scholar
  11. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    O. Burkat and B. Steffen. Composition, decomposition and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89–125, 1995.MathSciNetGoogle Scholar
  13. 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. 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. 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. 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. 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. 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. 19.
    J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts, 1979.zbMATHGoogle Scholar
  20. 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. 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. 22.
    D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL’97, Paris, 1997.Google Scholar
  23. 23.
    G.L. Peterson. Myths about the mutual exclusion problem. Info. Proc. Lett., 12(3):115, 1981.Google Scholar
  24. 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. 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.CrossRefMathSciNetGoogle Scholar
  26. 26.
    G. Senizergues. The equivalence problem for deterministic pushdown automata is decidable. volume 1256 of LNCS, p. 671–681, 1997.Google Scholar
  27. 27.
    E. Shahar. The tlv system and its application. Master’s thesis,Weizmann Institute, 1996.Google Scholar
  28. 28.
    Colin Stirling. Decidability of dpda equivalence. FODDACS’01, LNCS Springer-Verlag, 2001.Google Scholar
  29. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Dana Fisman
    • 1
  • Amir Pnueli
    • 1
  1. 1.Dept of Computer ScienceThe Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations