Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the cumulative weight while reaching a target. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers in real-time systems. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. A small restriction also allows us to obtain a class of decidable weighted timed games with negative weights and an arbitrary number of clocks. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation/computation schema over these classes. We also consider the special case of untimed weighted games, where the same fragments are solvable in polynomial time: this contrasts with the pseudo-polynomial complexity, known so far, for weighted games without restrictions.

翻译：加权定时博弈是两名玩家在配备权重的定时自动机上进行零和博弈，其中一方希望在到达目标的同时最小化累积权重。从反应式综合角度出发，这种定时博弈的定量扩展使得我们能够衡量实时系统中控制器的质量。加权定时博弈以难以处理著称，且即使限制为非负权重也会迅速变得不可判定。针对非负权重，Bouyer、Jaziri和Markey在2015年提出了可分析的最大类别。尽管值问题不可判定，但作者展示了如何通过考虑具有精细化粒度的区域来近似该值。在本研究中，我们将该类别扩展到包含负权重（例如用于建模能量），并证明其值仍能以相同复杂度进行近似。通过添加一个小限制，我们还获得了一类可判定的、包含负权重和任意数量时钟的加权定时博弈。此外，我们表明，依赖值迭代范式的符号算法可作为这些类别的近似/计算模式。我们还考虑了无时间加权博弈的特例，其中相同片断可在多项式时间内求解：这与目前已知的无限制加权博弈的伪多项式复杂度形成对比。