一句话：证明允许任意权重（含负权）的单时钟加权时间博弈可判定，并可在指数时间内计算值函数。
加权时间博弈（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).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2207-01608,
title = {Decidability of One-Clock Weighted Timed Games with Arbitrary Weights},
author = {Benjamin Monmege and Julie Parreaux and Pierre-Alain Reynier},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:8)2025}
}