TY - GEN
T1 - R-automata
AU - Abdulla, Parosh Aziz
AU - Krcal, Pavel
AU - Yi, Wang
PY - 2008
Y1 - 2008
N2 - We introduce R-automata - finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. 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. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12]- a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Büchi acceptance conditions.
AB - We introduce R-automata - finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. 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. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12]- a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Büchi acceptance conditions.
UR - https://www.scopus.com/pages/publications/54249108468
U2 - 10.1007/978-3-540-85361-9_9
DO - 10.1007/978-3-540-85361-9_9
M3 - 会议稿件
AN - SCOPUS:54249108468
SN - 354085360X
SN - 9783540853602
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 67
EP - 81
BT - CONCUR 2008 - Concurrency Theory - 19th International Conference, CONCUR 2008, Proceedings
T2 - 19th International Conference on Concurrency Theory, CONCUR 2008
Y2 - 19 August 2008 through 22 August 2008
ER -