Quantitative Strategy Templates

TL;DR

The paper introduces Quantitative Strategy Templates (QaSTels) as a quantitative extension of permissive templates to energy and mean-payoff games, providing edge-based representations and synthesis algorithms that yield winning, maximally permissive (for energy) or finitely permissive (for mean-payoff) templates. QaSTels enable runtime adaptation by allowing decisions to be reconfigured on-the-fly based on current energy credits and observed conditions, and they can be combined with bounded PeSTels into MiSTels to handle mixed quantitative-qualitative objectives, albeit with limited straightforward compositionality. An edge-based value iteration framework computes the edge-optimal QaSTel in $O(|V| imes|E| imes W)$ time and supports extraction of a corresponding positional strategy in $O(|E|)$; combined templates can be updated incrementally and hot-started to incorporate new objectives. The empirical study, using a SYNTCOMP-derived benchmark, demonstrates QaSTels’ runtime robustness and the practical benefits of incremental MiSTel synthesis, while acknowledging completeness limitations in the mixed-objective setting. Overall, the work provides foundational theory, practical algorithms, and evidence that strategy templates offer robust, adaptable control for CPS design under mixed quantitative and qualitative objectives.

Abstract

This paper presents (permissive) \emph{Quantitative Strategy Templates} (QaSTels) to succinctly represent infinitely many winning strategies in two-player energy and mean-payoff games. This transfers the recently introduced concept of \emph{Permissive (qualitative) Strategy Templates} (PeSTels) for $ω$-regular games to games with quantitative objectives. We provide the theoretical and algorithmic foundations of (i) QaSTel synthesis, and (ii) their (incremental) combination with PeSTels for games with mixed quantitative and qualitative objectives. Using a prototype implementation of our synthesis algorithms, we demonstrate empirically that QaSTels extend the advantageous properties of strategy templates over single winning strategies -- known from PeSTels -- to games with (additional) quantitative objectives. This includes (i) the enhanced robustness of strategies due to their runtime-adaptability, and (ii) the compositionality of templates w.r.t. incrementally arriving objectives. We use control-inspired examples to illustrate these superior properties of QaSTels for CPS design.

Figures (5)

• Figure 1: Example of an energy game (right top) with the computation for the edge-based value iteration (left) and the optimal QaSTel (right bottom).
• Figure 2: Mean-payoff game with $\cobuchi(\{a, c\})$ .
• Figure 3: Plots summarizing the experimental evaluations. Bigger figures can be found in the appendix.
• Figure 4: Plots summarizing the experimental evaluations.
• Figure :

Theorems & Definitions (46)

• definition thmcounterdefinition: Quantitative Strategy Template (QaSTel)
• definition thmcounterdefinition
• definition thmcounterdefinition: Winning QaSTel
• definition thmcounterdefinition: Maximal Permissiveness
• proposition thmcounterproposition
• proposition thmcounterproposition
• remark thmcounterremark
• theorem thmcountertheorem
• theorem thmcountertheorem
• theorem thmcountertheorem