论文标题
具有任意权重的一局加权定时游戏的可判决性
Decidability of One-Clock Weighted Timed Games with Arbitrary Weights
论文作者
论文摘要
加权定时游戏（简称WTG）是描述涉及实时问题的控制器合成问题的最广泛使用的模型。不幸的是，众所周知，它们是困难的，而且总体上是不可决定的。结果，一个锁定的WTG吸引了很多关注，尤其是因为只有允许非负重的重量时，它们是可以决定的。但是，当考虑任意权重时，尽管最近有几项工作，但它们的可判性状态仍然未知。在本文中，我们积极地解决了这个问题，并表明可以在指数时间（如果重量为单一编码）计算值函数。
Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTGs have attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).
