Deciding upperboundedness of Z -CCRA
A cost register automaton (CRA) over is a DFA equipped with a finite number of registers that take values in . Each transition induces a transformation of the registers formulated with and ; for instance . Accepting states can then output one of the registers. Consider the model in which: Each update uses only 's and addition with constants , For each transition, no register appears twice on the right-hand side of the updates. This model, which we call -CCRA (the extra C standing for copyless ), can express for instance:
but couldn't express ---this would require either copying , or adding two registers. For weighted automata people, note that this model is equivalent to this, where is a deterministic WA over : In [1], we showed that equivalence is undecidable for that model (even, and this is much more interesting, when restricted to ). We also showed that it is undecidable, given a -CCRA, to decide whether the function it expresses is always negative. Question: Is it decidable, given a -CCRA, whether the function it expresses is upper-bounded? That is, whether . [1] S. Almagor, M. Cadilhac, F. Mazowiecki, G. A. Pérez. Weak Cost Register Automata are Still Powerful. DLT'18. https://arxiv.org/abs/1804.06336
