Skip to main content
SpringerLink
Log in

Witness Runs for Counter Machines

  • Conference paper
Frontiers of Combining Systems (FroCoS 2013)

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

Included in the following conference series:

Abstract

In this paper, we present recent results about the verification of counter machines by using decision procedures for Presburger arithmetic. We recall several known classes of counter machines for which the reachability sets are Presburger-definable as well as temporal logics with arithmetical constraints. We discuss issues related to flat counter machines, path schema enumeration, and the use of SMT solvers.

Work partially supported by the EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF).

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. Atig, M.F., Habermehl, P.: On Yen’s path logic for Petri nets. IJFCS 22(4), 783–799 (2011)

    MathSciNet  MATH  Google Scholar 

  2. Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. I & C 127(2), 91–101 (1996)

    MathSciNet  MATH  Google Scholar 

  3. Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists Are Counter Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517–531. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)

    Article  Google Scholar 

  5. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Bersani, M.M., Demri, S.: The complexity of reversal-bounded model-checking. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 71–86. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Bruyère, V., Dall’Olio, E., Raskin, J.-F.: Durations, parametric model-checking in timed automata with Presburger arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 687–698. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 1995, pp. 123–133 (1995)

    Google Scholar 

  9. Berman, L.: The complexity of logical theories. TCS 11, 71–78 (1980)

    Article  MATH  Google Scholar 

  10. Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: TIME 2010, pp. 43–50. IEEE (2010)

    Google Scholar 

  12. Bozzelli, L., Gascon, R.: Branching-time temporal logic extended with qualitative Presburger constraints. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 197–211. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 337–351. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227–242. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. FI 91(2), 275–303 (2009)

    MathSciNet  MATH  Google Scholar 

  16. Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 611–625. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Biehl, M., Klarlund, N., Rauhe, T.: MONA: Decidable arithmetic in practice. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 459–462. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  18. Bojańczyk, M., Lasota, S.: An extension of data automata that captures XPath. In: LICS 2010, pp. 243–252. IEEE (2010)

    Google Scholar 

  19. Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Université de Liège (1999)

    Google Scholar 

  20. Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 88–103. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108–119. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. Frontiers in Artificial Intelligence and Applications, vol. 185, ch. 26, pp. 825–885. IOS Press (2008)

    Google Scholar 

  23. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0 (September 2012), http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf

  24. Boigelot, B., Wolper, P.: Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 55–67. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  25. Boigelot, B., Wolper, P.: Verifying systems with infinite but regular state spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  26. Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262–276. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press (2000)

    Google Scholar 

  28. Comon, H., Jurski, Y.: Multiple counter automata, safety analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of CTL* with constraints. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 455–469. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  30. Conchon, S.: SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Habilitation à Diriger des Recherches, Université Paris-Sud (2012)

    Google Scholar 

  31. Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Learning 7, 91–99 (1972)

    MATH  Google Scholar 

  32. Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. I & C 205(3), 380–415 (2007)

    MathSciNet  MATH  Google Scholar 

  33. Demri, S., Dhar, A.K., Sangnier, A.: Taming Past LTL and Flat Counter Systems. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 179–193. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  34. Demri, S., Dhar, A.K., Sangnier, A.: On the complexity of verifying regular properties on flat counter systems, In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 162–173. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  35. Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking \(\textsf{CTL}^{*}\) over flat Presburger counter systems. JANCL 20(4), 313–344 (2010)

    MATH  Google Scholar 

  36. Demri, S., Gascon, R.: Verification of qualitative Z constraints. TCS 409(1), 24–40 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  37. Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. JLC 19(6), 1541–1575 (2009)

    MathSciNet  MATH  Google Scholar 

  38. Demri, S., Lazić, R., Nowak, D.: On the freeze quantifier in constraint LTL: decidability and complexity. I & C 205(1), 2–24 (2007)

    MATH  Google Scholar 

  39. Demri, S., Lazić, R., Sangnier, A.: Model checking memoryful linear-time logics over one-counter automata. TCS 411(22-24), 2298–2316 (2010)

    Article  MATH  Google Scholar 

  40. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  41. Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 115–129. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  42. Fitting, M.: Modal logic between propositional and first-order. JLC 12(6), 1017–1026 (2002)

    MathSciNet  MATH  Google Scholar 

  43. Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  44. Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 213–227. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  45. Fischer, M., Rabin, M.: Super-exponential complexity of Presburger arithmetic. In: Complexity of Computation. SIAM-AMS proceedings, vol. 7, pp. 27–42. AMS (1974)

    Google Scholar 

  46. Ferrante, J., Rackoff, C.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer (1979)

    Google Scholar 

  47. Fribourg, L.: Petri nets, flat languages and linear arithmetic. In: 9th Workshop on Functional and Logic Programming (WFLP), pp. 344–365 (2000)

    Google Scholar 

  48. Finkel, A., Schnoebelen, P.: Well-structured transitions systems everywhere! TCS 256(1-2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  49. Finkel, A., Sangnier, A.: Reversal-bounded counter machines revisited. In: Ochmański, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol. 5162, pp. 323–334. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  50. Figueira, D., Segoufin, L.: Future-looking logics on data words and trees. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 331–343. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  51. Gurari, E., Ibarra, O.: The complexity of decision problems for finite-turn multicounter machines. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 495–505. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  52. Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 362–378. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  53. Goranko, V.: Temporal logic with reference pointers. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS (LNAI), vol. 827, pp. 133–148. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  54. Grädel, E.: Subclasses of Presburger arithmetic and the polynomial-time hierarchy. TCS 56, 289–301 (1988)

    Article  MATH  Google Scholar 

  55. German, S., Sistla, P.: Reasoning about systems with many processes. JACM 39(3), 675–735 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  56. Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  57. Henzinger, T.: Half-order modal logic: how to prove real-time properties. In: PODC 1990, pp. 281–296. ACM Press (1990)

    Google Scholar 

  58. Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743–759. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  59. Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. TCS 8, 135–159 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  60. Howell, R.R., Rosier, L.E.: An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. JCSS 34(1), 55–74 (1987)

    MathSciNet  MATH  Google Scholar 

  61. Howell, R.R., Rosier, L.E.: Problems concerning fairness and temporal logic for conflict-free petri nets. TCS 64, 305–329 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  62. Hunt, H., Rosenkrantz, D., Szymanski, T.: On the equivalence, containment, and covering problems for the regular and context-free languages. JCSS 12, 222–268 (1976)

    MathSciNet  MATH  Google Scholar 

  63. Ibarra, O.: Reversal-bounded multicounter machines and their decision problems. JACM 25(1), 116–133 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  64. Jančar, P.: Decidability of a temporal logic problem for Petri nets. TCS 74(1), 71–93 (1990)

    Article  MATH  Google Scholar 

  65. Karp, R.M., Miller, R.E.: Parallel program schemata. JCSS 3(2), 147–195 (1969)

    MathSciNet  MATH  Google Scholar 

  66. Kosaraju, R.: Decidability of reachability in vector addition systems. In: STOC 1982, pp. 267–281 (1982)

    Google Scholar 

  67. Leroux, J.: Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l’outil FAST. PhD thesis, ENS de Cachan, France (2003)

    Google Scholar 

  68. Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS 2009, pp. 4–13. IEEE (2009)

    Google Scholar 

  69. Leroux, J.: Presburger counter machines. Habilitation à Diriger des Recherches, Université Bordeaux (2012)

    Google Scholar 

  70. Leroux, J.: Presburger Vector Addition Systems. In: LICS 2013, pp. 23–32. IEEE (2013)

    Google Scholar 

  71. Lipton, R.J.: The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University (1976)

    Google Scholar 

  72. Lisitsa, A., Potapov, I.: Temporal logic with predicate λ-abstraction. In: TIME 2005, pp. 147–155. IEEE (2005)

    Google Scholar 

  73. Leroux, J., Point, G.: TaPAS: The Talence Presburger Arithmetic Suite. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 182–185. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  74. Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489–503. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  75. Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM ToCL 5(4), 669–705 (2004)

    Article  MathSciNet  Google Scholar 

  76. Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal of Computing 13(3), 441–460 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  77. Mayr, R.: Undecidable problems in unreliable computations. TCS 297(1-3), 337–354 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  78. Minsky, M.: Recursive unsolvability of Post’s problems of ‘tag’ and other topics in theory of Turing machines. Annals of Mathematics 74(3), 437–455 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  79. Minsky, M.: Computation, Finite and Infinite Machines. Prentice Hall (1967)

    Google Scholar 

  80. Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  81. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992)

    Google Scholar 

  82. Manna, Z., Pnueli, A.: Temporal verification of reative systems: safety. Springer (1995)

    Google Scholar 

  83. Mandel, A., Simon, I.: On finite semigroups of matrices. TCS 5(2), 101–111 (1977)

    Article  MathSciNet  Google Scholar 

  84. Oppen, D.: A \(2^{2^{2pn}}\) upper bound on the complexity of Presburger arithmetic. JCSS 16(3), 323–332 (1978)

    MathSciNet  MATH  Google Scholar 

  85. Ouaknine, J., Worrell, J.: On the Decidability of Metric Temporal Logic. In: LICS 2005, pp. 188–197. IEEE (2005)

    Google Scholar 

  86. Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE (1977)

    Google Scholar 

  87. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congrès de Mathématiciens des Pays Slaves, Warszawa, pp. 92–101 (1929)

    Google Scholar 

  88. Pugh, W.: A practical algorithm for exact array dependence analysis. Communications of the ACM 35(8), 102–114 (1992)

    Article  Google Scholar 

  89. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  90. Reutenauer, C.: The mathematics of Petri nets. Masson and Prentice (1990)

    Google Scholar 

  91. Reddy, C., Loveland, W.: Presburger arithmetic with bounded quantifier alternation. In: STOC 1978, pp. 320–325. ACM Press (1978)

    Google Scholar 

  92. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. IPL 83, 251–261 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  93. Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  94. Shostak, R.: A practical decision procedure for arithmetic with function symbols. JACM 26(2), 351–360 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  95. Suzuki, N., Jefferson, D.: Verification Decidability of Presburger Array Programs. JACM 27(1), 191–205 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  96. Segoufin, L., Torunczyk, S.: Automata based verification over linearly ordered data domains. In: STACS 2011, pp. 81–92 (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. New York University, USA

    Clark Barrett, Stéphane Demri & Morgan Deters

  2. LSV, CNRS, France

    Stéphane Demri

Authors
  1. Clark Barrett
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stéphane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Morgan Deters
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LORIA, Inria Nancy Grand Est, Université de Lorraine, 615 rue du Jardin Botanique, 54602, Villers-les-Nancy, France

    Pascal Fontaine

  2. LORIA, Inria Nancy Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Christophe Ringeissen

  3. School of Computer Science, The University of Manchester, Oxford Rd, Kilburn Building, M13 9PL, Manchester, UK

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barrett, C., Demri, S., Deters, M. (2013). Witness Runs for Counter Machines. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40885-4_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40884-7

  • Online ISBN: 978-3-642-40885-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation