2026-07-26T01:01:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19415 2024-03-06T11:03:59Z ddc:004 open_access

Counter Machines with Infrequent Reversals Finkel, Alain Krishna, Shankara Narayanan Madnani, Khushraj Majumdar, Rupak Zetzsche, Georg Counter machines reversal-bounded reachability decidability complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alain Finkel and Shankara Narayanan Krishna and Khushraj Madnani and Rupak Majumdar and Georg Zetzsche 2023 Is Part Of LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2023.42 urn:nbn:de:0030-drops-194152 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.42 eng https://creativecommons.org/licenses/by/4.0/legalcode