Document Open Access Logo

Boundedness of Cost Register Automata over the Integer Min-Plus Semiring

Authors Andrei Draghici , Radosław Piórkowski , Andrew Ryzhikov

PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.20.pdf
  • Filesize: 1.07 MB
  • 23 pages

Document Identifiers

Author Details

Andrei Draghici
  • Department of Computer Science, University of Oxford, UK
Radosław Piórkowski
  • Department of Computer Science, University of Oxford, UK
Andrew Ryzhikov
  • Department of Computer Science, University of Oxford, UK

Funding

All authors are supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite As Get BibTex

Andrei Draghici, Radosław Piórkowski, and Andrew Ryzhikov. Boundedness of Cost Register Automata over the Integer Min-Plus Semiring. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.20

Abstract

Cost register automata (CRAs) are deterministic automata with registers taking values from a fixed semiring. A CRA computes a function from words to values from this semiring. CRAs are tightly related to well-studied weighted automata. Given a CRA, the boundedness problem asks if there exists a natural number N such that for every word, the value of the CRA on this word does not exceed N. This problem is known to be undecidable for the class of linear CRAs over the integer min-plus semiring (ℤ∪{+∞}, min, +), but very little is known about its subclasses. In this paper, we study boundedness of copyless linear CRAs with resets over the integer min-plus semiring. We show that it is decidable for such CRAs with at most two registers. More specifically, we show that it is, respectively, NL-complete and in coNP if the numbers in the input are presented in unary and binary. We also provide complexity results for two classes with an arbitrary number of registers. Namely, we show that for CRAs that use the minimum operation only in the output function, boundedness is PSPACE-complete if transferring values to other registers is allowed, and is coNP-complete otherwise. Finally, for each f_i in the hierarchy of fast-growing functions, we provide a stateless CRA with i registers whose output exceeds N only on runs longer than f_i(N). Our construction yields a non-elementary lower bound already for four registers.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantitative automata
Keywords
  • cost register automata
  • boundedness
  • decidability

Metrics

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

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? Information and Computation, 282:104651, 2022. URL: https://doi.org/10.1016/j.ic.2020.104651.
  2. Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki, and Guillermo A. Pérez. Weak cost register automata are still powerful. International Journal of Foundations of Computer Science, 31(6):689-709, 2020. URL: https://doi.org/10.1142/S0129054120410026.
  3. Rajeev Alur, Loris D'Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), pages 13-22, 2013. URL: https://doi.org/10.1109/LICS.2013.65.
  4. Rajeev Alur and Mukund Raghothaman. Decision problems for additive regular functions. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 37-48. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_7.
  5. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 6(2):28:1-28:36, 2010. URL: https://doi.org/10.1145/1721837.1721844.
  6. Jørgen Bang-Jensen and Gregory Z Gutin. Digraphs: theory, algorithms and applications. Springer Science & Business Media, 2008. Google Scholar
  7. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is pspace-complete. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  8. Michael Blondin, Christoph Haase, Filip Mazowiecki, and Mikhail A. Raskin. Affine extensions of integer vector addition systems with states. Log. Methods Comput. Sci., 17(3), 2021. URL: https://doi.org/10.46298/LMCS-17(3:1)2021.
  9. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Transactions on Computational Logic, 11(4):23:1-23:38, 2010. URL: https://doi.org/10.1145/1805950.1805953.
  10. Karel Culík and Jarkko Kari. Digital images and formal languages. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 599-616. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_10.
  11. Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, David Purser, and Markus A. Whiteland. The boundedness and zero isolation problems for weighted automata over nonnegative rationals. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 15:1-15:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533336.
  12. Laure Daviaud. Containment and equivalence of weighted automata: Probabilistic and max-plus cases. In Alberto Leporati, Carlos Martín-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - 14th International Conference, LATA 2020, Milan, Italy, March 4-6, 2020, Proceedings, volume 12038 of Lecture Notes in Computer Science, pages 17-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-40608-0_2.
  13. Laure Daviaud. Register complexity and determinisation of max-plus automata. ACM SIGLOG News, 7(2):4-14, 2020. URL: https://doi.org/10.1145/3397619.3397621.
  14. Laure Daviaud, Pierre-Alain Reynier, and Jean-Marc Talbot. A generalised twinning property for minimisation of cost register automata. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2016), pages 857-866, 2016. URL: https://doi.org/10.1145/2933575.2934549.
  15. Laure Daviaud and Andrew Ryzhikov. Universality and forall-exactness of cost register automata with few registers. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 40:1-40:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.40.
  16. Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69-86, 2007. URL: https://doi.org/10.1016/J.TCS.2007.02.055.
  17. Manfred Droste and Paul Gastin. Weighted automata and weighted logics. In Handbook of weighted automata, pages 175-211. Springer, 2009. Google Scholar
  18. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer Berlin, Heidelberg, 1st edition, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5.
  19. Manfred Droste and Dietrich Kuske. Weighted automata. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 113-150. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/Automata-1/4.
  20. Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979. Google Scholar
  21. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  22. Kosaburo Hashiguchi. New upper bounds to the limitedness of distance automata. Theor. Comput. Sci., 233(1-2):19-32, 2000. URL: https://doi.org/10.1016/S0304-3975(97)00260-0.
  23. Kosaburo Hashiguchi, Kenichi Ishiguro, and Shuji Jimbo. Decisability of the equivalence problem for finitely ambiguous automata. International Journal of Algebra and Computation, 12(03):445-461, 2002. URL: https://doi.org/10.1142/S0218196702000845.
  24. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  25. Daniel Kirsten and Sylvain Lombardy. Deciding Unambiguity and Sequentiality of Polynomially Ambiguous Min-Plus Automata. In 26th International Symposium on Theoretical Aspects of Computer Science (STACS 2009), volume 3 of LIPIcs, pages 589-600, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1850.
  26. Ines Klimann, Sylvain Lombardy, Jean Mairesse, and Christophe Prieur. Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theoretical Computer Science, 327(3):349-373, 2004. URL: https://doi.org/10.1016/j.tcs.2004.02.049.
  27. Dexter Kozen. Lower bounds for natural proof systems. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 254-266. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  28. Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. International Journal of Algebra and Computation, 4(3):405-426, 1994. URL: https://doi.org/10.1142/S0218196794000063.
  29. Hing Leung and Viktor Podolskiy. The limitedness problem on distance automata: Hashiguchi’s method revisited. Theor. Comput. Sci., 310(1-3):147-158, 2004. URL: https://doi.org/10.1016/S0304-3975(03)00377-3.
  30. Ernst W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 238-246. ACM, 1981. URL: https://doi.org/10.1145/800076.802477.
  31. Filip Mazowiecki and Cristian Riveros. Maximal partition logic: Towards a logical characterization of copyless cost register automata. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 144-159. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CSL.2015.144.
  32. Filip Mazowiecki and Cristian Riveros. Copyless cost-register automata: Structure, expressiveness, and closure properties. Journal of Computer and System Sciences, 100:1-29, 2019. URL: https://doi.org/10.1016/j.jcss.2018.07.002.
  33. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, USA, 1967. Google Scholar
  34. Mehryar Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269-311, 1997. URL: https://aclanthology.org/J97-2003.
  35. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986. Google Scholar
  36. Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4(2):245-270, 1961. URL: https://doi.org/10.1016/S0019-9958(61)80020-X.
  37. Imre Simon. On semigroups of matrices over the tropical semiring. RAIRO Theor. Informatics Appl., 28(3-4):277-294, 1994. URL: https://doi.org/10.1051/ITA/1994283-402771.
  38. Michael Sipser. Introduction to the Theory of Computation. Course Technology, Boston, MA, third edition, 2013. Google Scholar
  39. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), pages 327-338, 1985. URL: https://doi.org/10.1109/SFCS.1985.12.
  40. Andreas Weber. Finite-valued distance automata. Theoretical Computer Science, 134(1):225-251, 1994. URL: https://doi.org/10.1016/0304-3975(94)90287-9.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact