Controller Synthesis for Parametric Timed Games

2025/06/18 by Mikael Bisgaard Dahlsen-Jensen, Dahlsen-Jensen, Mikael Bisgaard, Baptiste Fievet +5
Decision Sciences · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Simulation Techniques and Applications

paper · pdf · doi:10.48550/arxiv.2506.15532

openalex publication_date 2025/06/18 · openalex created_date 2025/10/19 · openalex updated_date 2026/07/28

Abstract

We present a (semi)-algorithm to compute winning strategies for parametric timed games. Previous algorithms only synthesized constraints on the clock parameters for which the game is winning. A new definition of (winning) strategies is proposed, and ways to compute them. A transformation of these strategies to (parametric) timed automata allows for building a controller enforcing them. The feasibility of the method is demonstrated by an implementation and experiments for the Production Cell case study.

Citations

• On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
• A theory of timed automata

Related

• On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
• Quantitative Games on Probabilistic Timed Automata
• A Zone-Based Algorithm for Timed Parity Games
• Timed Parity Games: Complexity and Robustness
• Synthesis of Robust Optimal Strategies in Weighted Timed Games