Document Open Access Logo

Counter Machines with Infrequent Reversals

Authors Alain Finkel , Shankara Narayanan Krishna , Khushraj Madnani , Rupak Majumdar , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.42.pdf
  • Filesize: 0.82 MB
  • 17 pages

Document Identifiers

Author Details

Alain Finkel
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, France
Shankara Narayanan Krishna
  • IIT Bombay, India
Khushraj Madnani
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

Alain Finkel was funded by the Institut Universitaire de France and the Agence Nationale de la Recherche, grant BraVAS (ANR-17-CE40-0028). Khushraj Madnani and Rupak Majumdar were supported in part by the Deutsche Forschungsgemeinschaft project 389792660 TRR 248-CPEC.

Cite AsGet BibTex

Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche. Counter Machines with Infrequent Reversals. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSTTCS.2023.42

Abstract

Bounding the number of reversals in a counter machine is one of the most prominent restrictions to achieve decidability of the reachability problem. Given this success, we explore whether this notion can be relaxed while retaining decidability. To this end, we introduce the notion of an f-reversal-bounded counter machine for a monotone function f: ℕ → ℕ. In such a machine, every run of length n makes at most f(n) reversals. Our first main result is a dichotomy theorem: We show that for every monotone function f, one of the following holds: Either (i) f grows so slowly that every f-reversal bounded counter machine is already k-reversal bounded for some constant k or (ii) f belongs to Ω(log(n)) and reachability in f-reversal bounded counter machines is undecidable. This shows that classical reversal bounding already captures the decidable cases of f-reversal bounding for any monotone function f. The key technical ingredient is an analysis of the growth of small solutions of iterated compositions of Presburger-definable constraints. In our second contribution, we investigate whether imposing f-reversal boundedness improves the complexity of the reachability problem in vector addition systems with states (VASS). Here, we obtain an analogous dichotomy: We show that either (i) f grows so slowly that every f-reversal-bounded VASS is already k-reversal-bounded for some constant k or (ii) f belongs to Ω(n) and the reachability problem for f-reversal-bounded VASS remains Ackermann-complete. This result is proven using run amalgamation in VASS. Overall, our results imply that classical restriction of reversal boundedness is a robust one.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Counter machines
  • reversal-bounded
  • reachability
  • decidability
  • complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Philippe Schnoebelen. Flat acceleration in symbolic model checking. In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 474-488. Springer, 2005. URL: https://doi.org/10.1007/11562948_35.
  2. Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar H. Ibarra, Ian McQuillan, Lia Schütze, and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 240-264. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_12.
  3. Marcello M. Bersani and Stéphane Demri. The complexity of reversal-bounded model-checking. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 71-86. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_6.
  4. Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 114:1-114:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.114.
  5. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Affine Parikh automata. RAIRO Theor. Informatics Appl., 46(4):511-545, 2012. URL: https://doi.org/10.1051/ita/2012013.
  6. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Bounded Parikh automata. Int. J. Found. Comput. Sci., 23(8):1691-1710, 2012. URL: https://doi.org/10.1142/S0129054112400709.
  7. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. Int. J. Found. Comput. Sci., 24(7):1099-1116, 2013. URL: https://doi.org/10.1142/S0129054113400339.
  8. Michaël Cadilhac, Andreas Krebs, and Pierre McKenzie. The algebraic theory of Parikh automata. Theory Comput. Syst., 62(5):1241-1268, 2018. URL: https://doi.org/10.1007/s00224-017-9817-2.
  9. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular separability of Parikh automata. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 117:1-117:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
  10. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 24:1-24:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.24.
  11. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  12. Wojciech Czerwinski and Georg Zetzsche. An approach to regular separability in vector addition systems. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 341-354. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394776.
  13. Zhe Dang, Oscar H. Ibarra, and Pierluigi San Pietro. Liveness verification of reversal-bounded multicounter machines with a free counter. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference, Bangalore, India, December 13-15, 2001, Proceedings, volume 2245 of Lecture Notes in Computer Science, pages 132-143. Springer, 2001. URL: https://doi.org/10.1007/3-540-45294-X_12.
  14. Stéphane Demri and Arnaud Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In C.-H. Luke Ong, editor, 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, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 176-190. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_13.
  15. Alain Finkel and Arnaud Sangnier. Reversal-bounded counter machines revisited. In Edward Ochmanski and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008, Torun, Poland, August 25-29, 2008, Proceedings, volume 5162 of Lecture Notes in Computer Science, pages 323-334. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85238-4_26.
  16. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. Google Scholar
  17. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-recognizable omega-languages, 2023. URL: https://arxiv.org/abs/2307.07238.
  18. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh automata over infinite words. In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 40:1-40:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.40.
  19. Eitan M. Gurari and Oscar H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981, Proceedings, volume 115 of Lecture Notes in Computer Science, pages 495-505. Springer, 1981. URL: https://doi.org/10.1007/3-540-10843-2_39.
  20. Christoph Haase. Subclasses of Presburger arithmetic and the weak EXP hierarchy. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 47:1-47:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  21. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 743-759. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_60.
  22. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  23. John Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8(2):135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  24. Oscar H Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM (JACM), 25(1):116-133, 1978. Google Scholar
  25. Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan, and Richard A. Kemmerer. Conter machines: Decidable properties and applications to verification problems. In Mogens Nielsen and Branislav Rovan, editors, Mathematical Foundations of Computer Science 2000, 25th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings, volume 1893 of Lecture Notes in Computer Science, pages 426-435. Springer, 2000. URL: https://doi.org/10.1007/3-540-44612-5_38.
  26. Matthias Jantzen and Alexy Kurganskyy. Refining the hierarchy of blind multicounter languages and twist-closed trios. Inf. Comput., 185(2):159-181, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00087-7.
  27. Petr Jančar. Decidability of a temporal logic problem for Petri nets. Theor. Comput. Sci., 74(1):71-93, 1990. URL: https://doi.org/10.1016/0304-3975(90)90006-4.
  28. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pages 681-696. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_54.
  29. Michel Latteux. Cônes rationnels commutatifs. J. Comput. Syst. Sci., 18(3):307-333, 1979. URL: https://doi.org/10.1016/0022-0000(79)90039-4.
  30. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 307-316. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  31. Jérôme Leroux. Presburger vector addition systems. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 23-32. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.7.
  32. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  33. Jérôme Leroux, M. Praveen, Philippe Schnoebelen, and Grégoire Sutre. On functions weakly computable by pushdown Petri nets and related systems. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:15)2019.
  34. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  35. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  36. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: https://doi.org/10.1007/11562948_36.
  37. Marvin L. Minsky. Recursive unsolvability of Post’s problem of "tag" and other topics in theory of Turing machines. Annals of Mathematics, 74(3):437-455, 1961. URL: http://www.jstor.org/stable/1970290.
  38. Loic Pottier. Minimal solutions of linear Diophantine systems: Bounds and algorithms. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 162-173. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_94.
  39. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.123.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact