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.

Continue Reading →