Skip to main content
SpringerLink
Log in

Fast Infinite-State Model Checking in Integer-Based Systems

  • Conference paper
Computer Science Logic (CSL 2003)

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

Included in the following conference series:

Abstract

In this paper we discuss the use of logic for reachability analysis for infinite-state systems. Infinite-state systems are formalized using transition systems over a first-order structure. We establish a common ground relating a large class of algorithms by analyzing the connections between the symbolic representation of transition systems and formulas used in various reachability algorithms. We consider in detail the so-called guarded assignment systems and local reachability algorithms. We show how an implementation of local reachability algorithms and a new incremental algorithm for finding Hilbert’s base in the system BRAINresulted in much faster reachability checking than in systems using constraint libraries and decision procedures for Presburger’s arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160(1-2), 109–127 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Abdulla, P.A., Jonsson, B.: Ensuring completeness of symbolic verification methods for infinite-state systems. Theoretical Computer Science 256, 145–167 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  3. Ajili, F., Contejean, E.: Avoiding slack variables in the solving of linear Diophantine equations and inequations. Theoretical Computer Science 173(1), 183–208 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  4. Beltyukov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility (in Russian). Zapiski Nauchnyh Seminarov LOMI 60, 15–28 (1976); English translation in Journal of Soviet Mathematics

    Google Scholar 

  5. Bjørner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University (1998)

    Google Scholar 

  6. Bjørner, N.S.: Reactive verification with queues. In: ARO/ONR/NSF/DARPA Workshop on Engineering Automation for Computer-Based Systems, Carmel, CA, pp. 1–8 (1998)

    Google Scholar 

  7. Bultan, T.: Action Language: a specification language for model checking reactive systems. In: ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, Limerick, Ireland, pp. 335–344. ACM, New York (2000)

    Chapter  Google Scholar 

  8. Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems 21(4), 747–789 (1999)

    Article  Google Scholar 

  9. Contejean, E., Devie, H.: An efficient incremental algorithm for solving of systems of linear Diophantine equations. Information and Computation 113(1), 143–172 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  10. Delzanno, G.: Automatic verification of parametrized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)

    MATH  Google Scholar 

  12. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)

    Article  MATH  Google Scholar 

  13. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), Trento, Italy, pp. 352–359. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

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

    Article  Google Scholar 

  15. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hy-Tech: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer 1(1–2), 110–122 (1997)

    MATH  Google Scholar 

  16. Henzinger, T.A., Majumdar, R.: A classification of symbolic state transition systems. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 13–34. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  17. Hilbert, D.: über die Theorie der algebraischen Formen. Mathematische Annalen 36, 473–534 (1890)

    Article  MathSciNet  Google Scholar 

  18. Kanellakis, P., Kuper, G.M., Revesz, P.Z.: Constraint query languages. Journal of Computer and System Sciences 51, 26–52 (1995)

    Article  MathSciNet  Google Scholar 

  19. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science 256(1-2), 93–112 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  20. Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  21. Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computations 32(3), 231–253 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  22. Lipshitz, L.: The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society 235, 271–283 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  23. Mart’janov, V.I.: Universal extended theories of integers. Algebra i Logika 16(5), 588–602 (1977)

    MathSciNet  Google Scholar 

  24. Podelski, A.: Model checking as constraint solving. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 22–37. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  25. Pugh, W.: Counting solutions to Presburger formulas: how and why. ACM SIGPLAN Notices 29(6), 121–134 (1994); Proceedings of the ACM SIGPLAN 1994 Conference on Programming Languages Design and Implementation (PLDI) (1994)

    Article  Google Scholar 

  26. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)

    Google Scholar 

  27. Rybina, T., Voronkov, A.: Using canonical representations of solutions to speed up infinitestate model-checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 386. Springer, Heidelberg (2002) (to appear)

    Chapter  Google Scholar 

  28. Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, Chichester (1998)

    MATH  Google Scholar 

  29. Tomás, A.P., Filgueiras, M.: An algorithm for solving systems of linear diophantine equations in naturals. In: Costa, E. (ed.) EPIA 1997. LNCS, vol. 1323, pp. 73–84. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  30. Voronkov, A.: An incremental algorithm for finding the basis of solutions to systems of linear Diophantine equations and inequations (January 2003) (unpublished)

    Google Scholar 

  31. Warren, D.S.: Memoing for logic programs. Communications of the ACM 35(3), 93–111 (1992)

    Article  Google Scholar 

  32. Yavuz-Kahveci, T., Tuncer, M., Bultan, T.: A library for composite symbolic representations. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 52–66. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester,  

    Tatiana Rybina & Andrei Voronkov

Authors
  1. Tatiana Rybina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Discrete Mathematics and Geometry, Technical University Vienna, Wiedner Hauptstrasse 8-10, A-1040, Wien, Austria

    Matthias Baaz

  2. Members of EACSL Jury for the Ackermann Award,  

    Johann A. Makowsky

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rybina, T., Voronkov, A. (2003). Fast Infinite-State Model Checking in Integer-Based Systems. In: Baaz, M., Makowsky, J.A. (eds) Computer Science Logic. CSL 2003. Lecture Notes in Computer Science, vol 2803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45220-1_46

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45220-1_46

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45220-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation