On the Interval-Bound Problem for Weighted Timed Automata
On the Interval-Bound Problem for Weighted Timed Automata
复制标题
关于加权时间自动机的区间界限问题
DOI：
10.1007/978-3-642-21254-3_36
复制
发表时间：
2011
影响因子：
4.9
通讯作者：
Karin Quaas
中科院分区：
文献类型：
--
作者：
Karin Quaas
加权定时自动机是配备有转移权重和位置权重率的定时自动机。这些权重可能是正数，也可能是负数，对应于某些资源的生产和消耗。我们考虑区间限制问题：是否存在无限运行，使得该运行的每个前缀的累积权重在某个给定的范围内？我们证明，如果加权定时自动机具有多个时钟和多个权重变量，则该问题是不可判定的。如果我们将时域限制为自然数，我们进一步证明该问题是 PSPACE 完全的。
A weighted timed automaton is a timed automaton equipped with weights on transitions and weight rates on locations. These weights may be positive or negative, corresponding to the production and consumption of some resources. We consider the interval-bound problem: does there exist an infinite run such that the accumulated weight for each prefix of the run is within some given bounds? We show that this problem is undecidable if the weighted timed automaton has more than one clock and more than one weight variable. We further prove that the problem is PSPACE-complete if we restrict the time domain to the natural numbers.