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完全的。