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

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

[thumbnail of accepted manuscript]
PDF (accepted manuscript) - Accepted Version
Download (423kB) | Preview


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.

Item Type: Book Section
Additional Information: Funding Information: Laure Daviaud: supported by the EPSRC grant EP/T018313/1. Andrew Ryzhikov: partially supported by the EPSRC grant EP/T018313/1 and by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).
Uncontrolled Keywords: cost register automata,decidability,forall-exact problem,universality,software,3*,possibly 4* ,/dk/atira/pure/subjectarea/asjc/1700/1712
Faculty \ School: Faculty of Science > School of Computing Sciences
Related URLs:
Depositing User: LivePure Connector
Date Deposited: 01 Aug 2023 08:30
Last Modified: 28 Oct 2023 01:29
URI: https://ueaeprints.uea.ac.uk/id/eprint/92739
DOI: 10.4230/LIPIcs.MFCS.2023.40


Downloads per month over past year

Actions (login required)

View Item View Item