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

Laure Daviaud, Andrew Ryzhikov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Downloads (Pure)


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 ForAll-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.
Original languageEnglish
Title of host publication48th International Symposium on Mathematical Foundations of Computer Science
Subtitle of host publicationMFCS 2023
EditorsJerome Leroux, Sylvain Lombardy, David Peleg
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages15
ISBN (Electronic)9783959772921
Publication statusPublished - Aug 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


  • cost register automata
  • decidability
  • forall-exact problem
  • universality

Cite this