@TechReport{ it:2008-016,
author = {Parosh Aziz Abdulla and Pavel Krcal and Wang Yi},
title = {R-automata},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2008},
number = {2008-016},
month = jun,
abstract = {We introduce \emph{R-automata} -- a model for analysis of
systems with resources which are consumed in small parts
but which can be replenished at once. An R-automaton is a
finite state machine which operates on a finite number of
unbounded counters (modeling the resources). The values of
the counters can be incremented, reset to zero, or left
unchanged along the transitions. We define the language
accepted by an R-automaton relative to a natural number $D$
as the set of words allowing a run along which no counter
value exceeds $D$. As the main result, we show decidability
of the universality problem, i.e., the problem whether
there is a number $D$ such that the corresponding language
is universal. The decidability proof is based on a
reformulation of the problem in the language of finite
monoids and solving it using the factorization forest
theorem. This approach extends the way in which the
factorization forest theorem was used to solve the
limitedness problem for distance automata in Simon, 1994.
We also show decidability of the non-emptiness problem and
the limitedness problem, i.e., whether there is a natural
number $D$ such that the corresponding language is
non-empty resp.\ all the accepted words can also be
accepted with counter values smaller than $D$. Finally, we
extend the decidability results to R-automata with B\"uchi
acceptance conditions.}
}