19.1 Deciding upperboundedness of \(\bbZ\)-CCRA

A cost register automaton (CRA) over \((\bbZ, \min, +)\) is a DFA equipped with a finite number of registers that take values in \(\bbZ\). Each transition induces a transformation of the registers formulated with \(\min\) and \(+\); for instance \(x \leftarrow \min\{x, y+3\} + z\). Accepting states can then output one of the registers.

Consider the model in which:

  • Each update uses only \(\min\)'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 $\bbZ$-CCRA (the extra C standing for copyless), can express for instance: \[f(a^{i_1}\#\ldots\#a^{i_n}) = \min \{i_1, \ldots, i_n\}\enspace,\] but couldn't express \(g(b^i\#w) = i + f(w)\) —this would require either copying \(i\), or adding two registers.

For weighted automata people, note that this model is equivalent to this, where \(\mathcal{W}\) is a deterministic WA over \((\mathbb{Z}, \min, +)\):

Sorry, your browser does not support SVG.

In [1], we showed that equivalence is undecidable for that model (even, and this is much more interesting, when restricted to \(\bbN\)). We also showed that it is undecidable, given a $\bbZ$-CCRA, to decide whether the function it expresses is always negative.

Question: Is it decidable, given a $\bbZ$-CCRA, whether the function it expresses is upper-bounded? That is, whether \((\exists c)(\forall w)[f(w) \leq c]\).

[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