Synthesis of Robust Optimal Strategies in Weighted Timed Games

TL;DR

This work studies robustness in Weighted Timed Games by introducing a parametric perturbation semantics that allows adversarial delay perturbations up to $p>0$ under a conservative framework. It establishes EXPTIME-completeness for fixed and existential robustness decision problems and proves decidability of the robust value for acyclic and divergent WTGs through a fixpoint characterization using the operator $ abla_p$ and a parametric, atomized representation via PVFs and shrunk DBMs. The approach combines region-based analysis, value iteration, and parametric symbolic techniques to compute robust values and synthesize near-optimal strategies. The results bridge robustness with quantitative objective synthesis in real-time games and open avenues for complexity refinements and fragment extensions with practical implications for robust controller synthesis under timing imprecision.

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.

Figures (5)

• Figure 1: An acyclic WTG with two clocks.
• Figure 2: Gadget used to encode the conservative semantics into the excessive one. Each transition $\delta\xspace =(\ell\xspace, g\xspace, Y\xspace, \ell\xspace')$ with $\ell\xspace\in L\xspace_{\mathsf{Min}\xspace}\xspace$ is replaced by the gadget. Symbols $w, w_0, w_1$ denote weights from $\mathcal{G}\xspace$. The new location $\ell\xspace^\delta\xspace$ of $\mathsf{Max}$ uses a fresh clock $x^{\mathsf{e}}$ to test the guard after the perturbation (as in the conservative semantics). The new location $\frownie$ is a deadlock (thus winning for $\mathsf{Max}$).
• Figure 3: On the left, we depict the partition defined from $\mathcal{E}\xspace = \{x_2 - 2\mathfrak{p}\xspace, 2 x_1 + x_2 - 2 + \mathfrak{p}\xspace, 2x_1 - x_2 + 1/2 \}$, for a small enough value of $\mathfrak{p}\xspace$. On the right, we depict the atomic partition induced by $\mathcal{E}\xspace$, and draw in red the added parametric affine expressions.
• Figure 4: Gadget used to define $\mathcal{G}\xspace^{\mathsf{e}}$ from $\mathcal{G}\xspace$. We detail how a transition $\delta\xspace =(\ell\xspace, g\xspace, Y\xspace, \ell\xspace')$ starting in a location belonging to $\mathsf{Min}$ is transformed. Symbols $w, w_0, w_1$ denote weights from $\mathcal{G}\xspace$. The new location $\ell\xspace^\delta\xspace$ of $\mathsf{Max}$ is urgent and tests the guard after the perturbation (as in the conservative semantics).
• Figure 5: Cells for the fixed-perturbation robust value functions computed for all locations of the acyclic WTG depicted in \ref{['fig:rob-valIt_ex-3']} when $p\xspace = \frac{1}{18}$.

Theorems & Definitions (51)

• Definition 1
• Definition 2
• Lemma 2
• Proposition 3
• Proposition 3
• Remark 4
• Lemma 4
• Proposition 5
• Theorem 6
• Lemma 6