Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. The synthesized strategies rely on a perfect measure of time elapse, which is not realistic in practice. In order to produce strategies tolerant to timing imprecisions, we rely on a notion of robustness first introduced for timed automata. More precisely, WTGs are two-player zero-sum games played in a timed automaton equipped with integer weights in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. In this work, we equip the underlying timed automaton with a semantics depending on some parameter (representing the maximal possible perturbation) in which the opponent of Min can in addition perturb delays chosen by Min. The robust value problem can then be stated as follows: given some threshold, determine whether there exists a positive perturbation and a strategy for Min ensuring to reach the target, with an accumulated weight below the threshold, whatever the opponent does. We provide the first decidability result for this robust value problem by computing the robust value function, in a parametric way, for the class of divergent WTGs (introduced to obtain decidability of the (classical) value problem in WTGs without bounding the number of clocks). To this end, we show that the robust value is the fixpoint of some operators, as is classically done for value iteration algorithms. We then combine in a very careful way two representations: piecewise affine functions introduced in [1] to analyse WTGs, and shrunk Difference Bound Matrices considered in [29] to analyse robustness in timed automata. Last, we also study qualitative decision problems and close an open problem on robust reachability, showing it is EXPTIME-complete for general WTGs.

翻译：加权时间博弈（简称WTG）是描述涉及实时问题的控制器综合问题最广泛使用的模型。所综合的策略依赖于对时间流逝的完美测量，这在实践中并不现实。为了产生容忍时间不精确性的策略，我们依赖于最初为时间自动机引入的鲁棒性概念。更准确地说，WTG是在配备整数权值的时间自动机上进行的两人零和博弈，其中一方（称为Min）希望在最小化累积权值的同时到达目标位置。在本工作中，我们为基础时间自动机配备了一种依赖于某个参数（表示最大可能扰动）的语义，在该语义中，Min的对手还可以额外扰动Min选择的延迟。鲁棒值问题可表述如下：给定某个阈值，确定是否存在一个正扰动以及Min的一个策略，使其无论对手如何行动，都能以低于阈值的累积权值确保到达目标。我们首次为这一鲁棒值问题提供了可判定性结果，通过以参数化方式计算了发散类WTG的鲁棒值函数（该类WTG是为了在不限制时钟数量的情况下获得其（经典）值问题的可判定性而引入的）。为此，我们证明鲁棒值是某些算子的不动点，这与值迭代算法的经典做法一致。然后我们以非常谨慎的方式结合了两种表示：文献[1]中为分析WTG引入的分段仿射函数，以及文献[29]中为分析时间自动机鲁棒性考虑的压缩差分约束矩阵。最后，我们还研究了定性决策问题，并解决了鲁棒可达性上的一个开放问题，证明了对于一般WTG，该问题是EXPTIME完全的。