Advertisement

Reasoning About Reversal-Bounded Counter Machines

  • Stéphane Demri
Chapter
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)

Abstract

In this paper, we present a short survey on reversal-bounded counter machines. It focuses on the main techniques for model-checking such counter machines with specifications expressed with formulae from some linear-time temporal logic. All the decision procedures are designed by translation into Presburger arithmetic. We provide a proof that is alternative to Ibarra’s original one for showing that reachability sets are effectively definable in Presburger arithmetic. Extensions to repeated control state reachability and to additional temporal properties are discussed in the paper. The article is written to the honor of Professor Ewa Orłowska and focuses on several topics that are developed in her works.

Keywords

Counter machines Verification Temporal logics Presburger arithmetic 

Notes

Acknowledgements

I would like to thank the anonymous reviewers for their suggestions and remarks that help me improve the quality of the document.

References

  1. Atig, M. F. (2010). Global model checking of ordered multi-pushdown systems. In K. Lodaya & M. Mahajan (Eds.), IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010 (Vol. 8, pp. 216–227). LIPIcs. Chennai: Schloss Dagstuhl - Leibniz- Zentrum für Informatik.Google Scholar
  2. Baker, B. S. & Book, R. V. (1974). Reversal-bounded multipushdown machines. Journal of Computer and System Sciences, 8(3), 315–332.CrossRefGoogle Scholar
  3. Balbiani, P. & Orłowska, E. (1999). A hierarchy of modal logics with relative accessibility relations. Journal of Applied Non-Classical Logics: Special Issue in the Memory of George Gargov, 9(2–3), 303–328.CrossRefGoogle Scholar
  4. Berman, L. (1980). The complexity of logical theories. Theoretical Computer Science, 11, 71–77.CrossRefGoogle Scholar
  5. Bersani, M. M. & Demri, S. (2011). The complexity of reversal-bounded model-checking. In C. Tinelli & V. Sofronie-Stokkermans (Eds.), Proceedings of Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011 (Vol. 6989, pp. 71–86). Lecture Notes in Computer Science. Saarbrücken, Germany.Google Scholar
  6. Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., & Zhu, Y. (2003). Bounded model checking. Advances in Computers, 58, 117–148.CrossRefGoogle Scholar
  7. Blattner, M. & Latteux, M. (1981). Parikh-bounded languages. In S. Even & O. Kariv (Eds.), Proceedings of Automata, Languages and Programming, 8th Colloquium (Vol. 115, pp. 316–323). Lecture Notes in Computer Science. Acre: Springer.CrossRefGoogle Scholar
  8. Borosh, I. & Treybig, L. B. (1976). Bounds on positive integral solutions of linear Diophantine equations. Proceedings of the American Mathematical Society, 55(2), 299–304.CrossRefGoogle Scholar
  9. Boigelot, B. (1999). Symbolic Methods for Exploring Infinite State Spaces, Doctoral dissertation, Université de Liège.Google Scholar
  10. Bojańczyk, M. & Lasota, S. (2010). An extension of data automata that captures XPath. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 (pp. 243–252). Edinburgh: IEEE Computer Society.Google Scholar
  11. Bouajjani, A., Echahed, R., & Habermehl, P. (1995). On the verification problem of nonregular properties for nonregular processes. Proceedings, 10th annual IEEE symposium on logic in computer science (pp. 123–133). San Diego: IEEE Computer Society.Google Scholar
  12. Bozga, M., Iosif, R., & Konecný, F. (2010). Fast acceleration of ultimately periodic relations. In T. Touili, B. Cook, & P. B. Jackson (Eds.), 22nd International Conference, CAV 2010 Proceedings of Computer Aided Verification, (Vol. 6174, pp. 227–242). Lecture Notes in Computer Science. Edinburgh: Springer.Google Scholar
  13. Bresolin, D., Golińska-Pilarek, J., & Orłowska, E. (2006). A relational dual tableaux for interval temporal logics. Journal of Applied Non-classical Logics, 16(3–4), 251–277.CrossRefGoogle Scholar
  14. Bruyère, V., Dall’Olio, E., & Raskin, J.-F. (2003). Durations, parametric modelchecking in timed automata with presburger arithmetic. In H. Alt & M. Habib (Eds.), Proceedings of STACS 2003, 20th Annual Symposium on Theoretical Aspects of Computer Science (Vol. 2607, pp. 687–698). Lecture Notes in Computer Science. Berlin: Springer.Google Scholar
  15. Cadilhac, M., Finkel, A., & McKenzie, P. (2011). On the expressiveness of Parikh automata and related models. In R. Freund, M. Holzer, C. Mereghetti, F. Otto, & B. Palano (Eds.), Proceedings of the 3rd Workshop on Non-classical Models of Automata and Applications (NCMA’11) (Vol. 282, pp. 103–119). Austrian Computer Society.Google Scholar
  16. Čerāns, K. (1994). Deciding properties of integral relational automata. In S. Abiteboul & E. Shamir (Eds.), Proceedings of Automata, Languages and Programming, 21st International Colloquium, ICALP’94 (Vol. 820, pp. 35–46). Lecture Notes in Computer Science. Jerusalem: Springer.CrossRefGoogle Scholar
  17. Chan, T.-h. (1981). Reversal complexity of counter machines. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing (pp. 146–157). Milwaukee: ACM.Google Scholar
  18. Comon, H. & Cortier, V. (2000). Flatness is not a weakness. In P. Clote & H. Schwichtenberg (Eds.), Proceedings of 14th Annual Conference of the Computer Science Logic, EACSL (Vol. 1862, pp. 262–276). Lecture Notes in Computer Science. Fischbachau: Springer.Google Scholar
  19. Comon, H. & Jurski, Y. (1998). Multiple counter automata, safety analysis and Presburger arithmetic. In A. J. Hu & M. Y. Vardi (Eds.), Proceedings of the 10th International Conference Computer Aided Verification, CAV’98 (Vol. 1427, pp. 268–279). Lecture Notes in Computer Science. Vancouver: Springer.Google Scholar
  20. Czerwiński, W., Hofman, P., & Lasota, S. (2013). Reachability problem for weak multi-pushdown automata. Logical Methods in Computer Science, 9(3).Google Scholar
  21. Dang, Z., Ibarra, O. H., Bultan, T., Kemmerer, R. A., & Su, J. (2000). Binary reachability analysis of discrete pushdown timed automata. In E. A. Emerson & A. P. Sistla (Eds.), Proceedings of the 12th International Conference of the Computer Aided Verification, CAV 2000 (Vol. 1855, pp. 69–84). Lecture Notes in Computer Science. Chicago: Springer.CrossRefGoogle Scholar
  22. Dang, Z., Ibarra, O. H., & Pietro, P. S. (2001). Liveness verification of reversal-bounded multicounter machines with a free counter. In R. Hariharan, M. Mukund, & V. Vinay (Eds.), Proceedings of FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference (Vol. 2245, pp. 132–143). Lecture Notes in Computer Science. Bangalore: Springer.CrossRefGoogle Scholar
  23. Dang, Z., Pietro, P. S., & Kemmerer, R. A. (2003). Presburger liveness verification of discrete timed automata. Theoretical Computer Science, 299(1–3), 413–438.CrossRefGoogle Scholar
  24. Demri, S. (2006). Linear-time temporal logics with Presburger constraints: An overview. Journal of Applied Non-Classical Logics, 16(3–4), 311–348.CrossRefGoogle Scholar
  25. Demri, S., Dhar, A. K., & Sangnier, A. (2013). On the complexity of verifying regular properties on flat counter systems, In F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, & D. Peleg (Eds.), Proceedings of Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, part II (Vol. 7966, pp. 162–173). Lecture Notes in Computer Science. Riga: Springer.CrossRefGoogle Scholar
  26. Demri, S., Dhar, A. K., & Sangnier, A. (2015). Taming past LTL and flat counter systems. Information and Computation, 242, 306–339.CrossRefGoogle Scholar
  27. Demri, S., Figueira, D., & Praveen, M. (2016). Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12(3).Google Scholar
  28. Demri, S., Goranko, V., & Lange, M. (2016). Temporal Logics in Computer Science: Finite-state Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge: Cambridge University Press.Google Scholar
  29. Demri, S. & Sangnier, A. (2010). When model-checking freeze LTL over counter machines becomes decidable. In C.-H. L. Ong (Ed.), Proceedings of Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 (Vol. 6014, pp. 176–190). Lecture Notes in Computer Science. Paphos: Springer.CrossRefGoogle Scholar
  30. Esparza, J. (1994). On the decidability of model checking for several \(\mu \)-calculi and Petri nets. In S. Tison (Ed.), Proceedings of Trees in Algebra and Programming –CAAP’94, 19th International Colloquium (Vol. 787, pp. 115–129). Lecture Notes in Computer Science. Edinburgh: Springer.Google Scholar
  31. Esparza, J. (1996). Decidability and complexity of Petri net problems – an introduction. In W. Reisig & G. Rozenberg (Eds.), Lectures on Petri nets I: Basic models, advances in Petri nets (Vol. 1491, pp. 374–428). Lecture Notes in Computer Science. The volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996. Berlin: Springer.CrossRefGoogle Scholar
  32. Esparza, J. & Ganty, P. (2011). Complexity of pattern-based verification for multithreaded programs. In T. Ball & M. Sagiv (Eds.), Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011 (pp. 499–510). Austin: ACM.Google Scholar
  33. Fariñas del Cerro, L. & Orłowska, E. (1985). DAL – a logic for data analysis. Theoretical Computer Science, 36, 251–264. Corrigendum: ibid. Fariñas del Cerro and Orłowska (1986).CrossRefGoogle Scholar
  34. Fariñas del Cerro, L. & Orłowska, E. (1986). DAL – a logic for data analysis: Corrigendum. Theoretical Computer Science, 47, 345.Google Scholar
  35. Finkel, A., Iyer, S. P., & Sutre, G. (2003). Well-abstracted transition systems: Application to FIFO automata. Information and Computation, 181(1), 1–31.CrossRefGoogle Scholar
  36. Finkel, A. & Leroux, J. (2002). How to compose Presburger-accelerations: Applications to broadcast protocols. In M. Agrawal & A. Seth (Eds.), Proceedings of FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd conference (Vol. 2556, pp. 145–156). Lecture Notes in Computer Science. Kanpur: Springer.CrossRefGoogle Scholar
  37. Finkel, A. & Sangnier, A. (2008). Reversal-bounded counter machines revisited. In E. Ochmański & J. Tyszkiewicz (Eds.), Proceedings of the 33rd International Symposium of the Mathematical Foundations of Computer Science 2008, MFCS 2008 (Vol. 5162, pp. 323–334). Lecture Notes in Computer Science. Toruń: Springer.Google Scholar
  38. Fribourg, L. (2000). Petri nets, flat languages and linear arithmetic. In M. Alpuente (Ed.), 9th International Workshop on Functional and Logic Programming, WFLP’00 (pp. 344–365). Spain: Benicassim.Google Scholar
  39. Fribourg, L. & Olsén, H. (1997). Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In A. W. Mazurkiewicz & J. Winkowski (Eds.), Proceedings of the 8th International Conference the CONCUR ’97: Concurrency Theory, (Vol. 1243, pp. 213–227). Lecture Notes in Computer Science. Warsaw: Springer.CrossRefGoogle Scholar
  40. Ginsburg, S. & Spanier, E. (1966). Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2), 285–296.CrossRefGoogle Scholar
  41. Gurari, E. M. & Ibarra, O. H. (1981). The complexity of decision problems for finite-turn multicounter machines. In S. Even & O. Kariv (Eds.), Proceedings of Automata, Languages and Programming, 8th Colloquium (Vol. 115, pp. 495–505). Lecture Notes in Computer Science. Acre (Akko): Springer.CrossRefGoogle Scholar
  42. Haase, C. (2014). Subclasses of Presburger arithmetic and the weak EXP hierarchy. In T. A. Henzinger & D. Miller (Eds.), Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (lics), CSL-LICS ’14 (pp. 47:1–47:10). Vienna: ACM.Google Scholar
  43. Haase, C. & Halfon, S. (2014). Integer vector addition systems with states. In J. Ouaknine, I. Potapov, & J. Worrell (Eds.), Proceedings of Reachability Problems – 8th International Workshop, RP 2014 (Vol. 8762, pp. 112–124). Lecture Notes in Computer Science. Oxford: Springer.Google Scholar
  44. Habermehl, P. (1997). On the complexity of the linear-time \(\mu \) -calculus for Petri nets. In P. Azéma & G. Balbo (Eds.), Proceedings of Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97 (Vol. 1248, pp. 102–116). Lecture Notes in Computer Science. Toulouse: Springer.Google Scholar
  45. Hague, M. & Lin, A. W. (2011). Model checking recursive programs with numeric data types. In G. Gopalakrishnan & S. Qadeer (Eds.), Proceedings of Computer Aided Verification –23rd International Conference, CAV 2011 (Vol. 6806, pp. 743–759). Lecture Notes in Computer Science. Snowbird: Springer.Google Scholar
  46. Howell, R. R. & Rosier, L. E. (1987). An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. Journal of Computer and System Sciences, 34(1), 55–74.CrossRefGoogle Scholar
  47. Howell, R. R. & Rosier, L. E. (1989). Problems concerning fairness and temporal logic for conflict-free Petri nets. Theoretical Computer Science, 64(3), 305–329.CrossRefGoogle Scholar
  48. Ibarra, O. H. (1974). A note on semilinear sets and bounded-reversal multihead pushdown automata. Information Processing Letters, 3(1), 25–28.CrossRefGoogle Scholar
  49. Ibarra, O. H. (1978). Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25(1), 116–133.CrossRefGoogle Scholar
  50. Ibarra, O. H., Su, J., Dang, Z., Bultan, T., & Kemmerer, R. A. (2002). Counter machines and verification problems. Theoretical Computer Science, 289(1), 165–189.CrossRefGoogle Scholar
  51. Jančar, P. (1990). Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 74(1), 71–93.CrossRefGoogle Scholar
  52. Karp, R. M. & Miller, R. E. (1969). Parallel program schemata. Journal of Computer and System Sciences, 3(2), 147–195.CrossRefGoogle Scholar
  53. Klaedtke, F. & Rueß, H. (2002). Parikh automata and monadic second-order logics with linear cardinality constraints. Technical report No. 177, Institute of Computer Science at Freiburg University.Google Scholar
  54. Kopczyński, E. & Widjaja To, A. (2010). Parikh images of grammars: Complexity and applications. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 (pp. 80–89). Edinburgh: IEEE Computer Society.Google Scholar
  55. Kosaraju, S. R. (1982). Decidability of reachability in vector addition systems (preliminary version). In H. R. Lewis, B. B. Simons, W. A. Burkhard, & L. H. Landweber (Eds.), Proceedings of the 14th Annual ACM Symposium on Theory of Computing (pp. 267–281). San Francisco: ACM.Google Scholar
  56. La Torre, S., Madhusudan, P., & Parlato, G. (2007). A robust class of context-sensitive languages. In Proceedings of the 22nd IEEE Symposium on Logic in Computer Science, LICS 2007 (pp. 161–170). Wrocław: IEEE Computer Society.Google Scholar
  57. Laroussinie, F., Meyer, A., & Petonnet, E. (2010). Counting LTL. In N. Markey & J. Wijsen (Eds.), TIME 2010–17th International Symposium on Temporal Representation and Reasoning (pp. 51–58). Paris France: IEEE Computer Society.Google Scholar
  58. Leroux, J. (2009). The general vector addition system reachability problem by Presburger inductive invariants. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009 (pp. 4–13). Los Angeles: IEEE Computer Society.Google Scholar
  59. Leroux, J. & Schmitz, S. (2015). Demystifying reachability in vector addition systems. 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 (pp. 56–67). Kyoto: IEEE Computer Society.Google Scholar
  60. Lipton, R. J. (1976). The reachability problem requires exponential space. Technical report No. 62, Department of Computer Science, Yale University.Google Scholar
  61. Manna, Z. & Pnueli, A. (1995). Temporal Verification of Reactive Systems – Safety. Berlin: Springer.CrossRefGoogle Scholar
  62. Mayr, E. W. (1984). An algorithm for the general Petri net reachability problem. SIAM Journal on Computing, 13(3), 441–460.CrossRefGoogle Scholar
  63. Minsky, M. (1961). Recursive unsolvability of Post’s problems of ’tag’ and other topics in theory of Turing machines. Annals of Mathematics, 74(3), 437–455.CrossRefGoogle Scholar
  64. Minsky, M. (1967). Computation, Finite and Infinite Machines. Prentice: Prentice Hall.Google Scholar
  65. Orłowska, E. (1973). Theorem Proving Systems., Dissertationes Mathematicae CIII Warsaw: Polish Scientific Publishers.Google Scholar
  66. Orłowska, E. (1985). Logic of nondeterministic information. Studia Logica, 44(1), 91–100.CrossRefGoogle Scholar
  67. Orłowska, E. (1988). Relational interpretation of modal logics. In H. Andreka, D. Monk, & I. Németi (Eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai (Vol. 54, pp. 443–471). Amsterdam: North Holland.Google Scholar
  68. Orłowska, E. (1989). Logic for reasoning about knowledge. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 35, 559–572.CrossRefGoogle Scholar
  69. Orłowska, E. (1993). Dynamic logic with program specifications and its relational proof system. Journal of Applied Non-Classical Logics, 3, 147–171.CrossRefGoogle Scholar
  70. Orłowska, E. (1995). Temporal logics in a relational framework. In L. Bolc & A. Szałas (Eds.), Time and Logic: a Computational Approach (pp. 249–277). University College London Press.Google Scholar
  71. Papadimitriou, C. H. (1981). On the complexity of integer programming. Journal of the ACM, 28(4), 765–768.CrossRefGoogle Scholar
  72. Parikh, R. (1966). On context-free languages. Journal of the ACM, 13(4), 570–581.CrossRefGoogle Scholar
  73. Pnueli, A. (1977). The temporal logic of programs. 18th Annual Symposium on Foundations of Computer Science (pp. 46–57). Providence: IEEE Computer Society.Google Scholar
  74. Presburger, M. (1929). Ü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 (pp. 92–101). Warsaw, Poland.Google Scholar
  75. Qadeer, S. & Rehof, J. (2005). Context-bounded model checking of concurrent software. In N. Halbwachs & L. D. Zuck (Eds.), Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 (Vol. 3440, pp. 93–107). Lecture Notes in Computer Science. Edinburgh: Springer.CrossRefGoogle Scholar
  76. Rackoff, C. (1978). The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6, 223–231.CrossRefGoogle Scholar
  77. Reutenauer, C. (1990). The Mathematics of Petri Nets. Masson and Prentice.Google Scholar
  78. Sangnier, A. (2008). Vérification de systèmes avec compteurs et pointeurs, Doctoral dissertation, LSV, ENS Cachan, France.Google Scholar
  79. Savitch, W. J. (1970). Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2), 177–192.CrossRefGoogle Scholar
  80. Schrijver, A. (1986). Theory of Linear and Integer Programming. New York: WileyGoogle Scholar
  81. Suzuki, N. & Jefferson, D. (1980). Verification decidability of Presburger array programs. Journal of the ACM, 27(1), 191–205.CrossRefGoogle Scholar
  82. Widjaja To, A. (2010). Model Checking Infinite-state Systems: Generic and Specific Approaches, Doctoral dissertation. School of Informatics, University of Edinburgh.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.LSV, CNRS, ENS Paris-SaclayUniversité Paris-SaclayCachan CedexFrance

Personalised recommendations