Synthesis of Robust Optimal Strategies in Weighted Timed Games

Abstract

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.