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).

翻译：加权时间博弈（简称WTG）是描述涉及实时问题的控制器综合问题中应用最广泛的模型。遗憾的是，这类博弈通常极其复杂，且一般情况下是不可判定的。因此，单时钟WTG受到了广泛关注，特别是因为已知在仅允许非负权重的情况下它们是可判定的。然而，当考虑任意权重时，尽管近期已有若干研究成果，其可判定性状态仍属未知。本文中，我们正面解决了该问题，并证明其值函数可在指数时间内计算得到（若权重采用一元编码）。