Document Open Access Logo

Universality and Forall-Exactness of Cost Register Automata with Few Registers

Authors Laure Daviaud , Andrew Ryzhikov

Thumbnail PDF


  • Filesize: 0.85 MB
  • 15 pages

Document Identifiers

Author Details

Laure Daviaud
  • School of Computing Sciences, University of East Anglia, Norwich, UK
Andrew Ryzhikov
  • Department of Computer Science, University of Oxford, UK

Cite AsGet BibTex

Laure Daviaud and Andrew Ryzhikov. Universality and Forall-Exactness of Cost Register Automata with Few Registers. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 40:1-40:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


The universality problem asks whether a given finite state automaton accepts all the input words. For quantitative models of automata, where input words are mapped to real values, this is naturally extended to ask whether all the words are mapped to values above (or below) a given threshold. This is known to be undecidable for commonly studied examples such as weighted automata over the positive rational (plus-times) or the integer tropical (min-plus) semirings, or equivalently cost register automata (CRAs) over these semirings. In this paper, we prove that when restricted to CRAs with only three registers, the universality problem is still undecidable, even with additional restrictions for the CRAs to be copyless linear with resets. In contrast, we show that, assuming the unary encoding of updates, the ∀-exact problem (does the CRA output zero on all the words?) for integer min-plus linear CRAs can be decided in polynomial time if the number of registers is constant. Without the restriction on the number of registers this problem is known to be PSPACE-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantitative automata
  • cost register automata
  • universality
  • forall-exact problem
  • decidability


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


  1. Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? Information and Computation, 282:104651, 2022. URL:
  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:
  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:
  4. 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:
  5. Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell. Polynomial automata: Zeroness and applications. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), pages 1-12, 2017. URL:
  6. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Transactions on Computational Logic, 11(4):23:1-23:38, 2010. URL:
  7. 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:
  8. Laure Daviaud. Register complexity and determinisation of max-plus automata. ACM SIGLOG News, 7(2):4-14, 2020. URL:
  9. Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When are emptiness and containment decidable for probabilistic automata? Journal of Computer and System Sciences, 119:78-96, 2021. URL:
  10. 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:
  11. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer Berlin, Heidelberg, 1st edition, 2009. URL:
  12. 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:
  13. 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:
  14. 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:
  15. 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:
  16. 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:
  17. 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:
  18. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, USA, 1967. Google Scholar
  19. Mehryar Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269-311, 1997. URL:
  20. Azaria Paz. Introduction to probabilistic automata. Academic Press, 1971. Google Scholar
  21. Marcel-Paul Schützenberger. On the definition of a family of automata. Information and Control, 4(2):245-270, 1961. URL:
  22. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In 5th Annual ACM Symposium on Theory of Computing (STOC 1973), pages 1-9, 1973. URL:
  23. 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:
  24. Andreas Weber. Finite-valued distance automata. Theoretical Computer Science, 134(1):225-251, 1994. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail