R-Automata
R-Automata
复制标题
R自动机
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
W. Yi
中科院分区：
文献类型：
--
作者：
P. Abdulla;P. Krcál;W. Yi
我们引入 R 自动机——有限状态机，它在有限数量的无界计数器上运行。计数器的值可以在转换过程中递增、重置为零或保持不变。例如，R 自动机可用于对具有资源（由计数器建模）的系统进行建模，这些资源会被小部分消耗，但可以立即补充。我们相对于自然数 Da 定义 R 自动机接受的语言，即允许运行的单词集合，其中没有计数器值超过 D。作为主要结果，我们显示了普遍性问题的可判定性，即是否存在数字 D 使得相应的语言是普遍的问题。我们提出了基于有限幺半群和因式分解森林定理的证明。该定理应用于 [12] 中的距离自动机——R 自动机的一种特殊情况，具有一个永不重置的计数器。作为第二个技术贡献，我们将可判定性结果扩展到具有 Buchi 接受条件的 R 自动机。
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 Das 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 Dsuch 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 Buchi acceptance conditions.