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年引入了最大可分析类别。尽管值问题不可判定，作者展示了如何通过考虑具有精细粒度的区域来近似该值。在本工作中，我们将此类扩展至包含负权重，从而允许建模诸如能量等场景，并证明该值仍可近似，且复杂度相同。一个小的限制还使我们能够获得一类可判定的、包含负权重和任意数量时钟的加权时间博弈。此外，我们展示了一种依赖于值迭代范式的符号算法，可作为这些类别上的近似/计算方案。我们还考虑了无时间加权博弈的特殊情况，其中相同的片段可在多项式时间内求解：这与此类无约束加权博弈迄今为止已知的伪多项式复杂度形成了对比。