Universality of R-automata with Value Copying

R-automata are finite state machines extended with counters which can be incremented or reset to zero along the transitions. The universality question asks whether there is a constant D such that all words are accepted by some run along which no counter exceeds D. It has been shown in [Parosh Abdulla, Pavel Krcal, and Wang Yi. R-automata. In Proc. of CONCUR'08., volume 5201 of LNCS, pages 67–81. Springer, 2008] that this question is decidable. In this paper, we add one more operation to R-automata, namely the operation which can copy the value of a counter into another one. The result of this paper is a reduction of the universality problem for R-automata with value copying to universality of R-automata, thus rendering the problem decidable. The reduction replaces copy operations by non-deterministic resets together with a mechanism ensuring that the number of such replacements is bounded between each two resets of a value.