Deciding the synthesis problem for hybrid games through bisimulation
Catalin Dima, Mariem Hammami, Youssouf Oualhadj, Régine Laleau
TL;DR
This work addresses the synthesis problem for hybrid games, showing that initialized singular games (ISR) can be reduced to timed games through a sequence of alternating bisimulations. The method passes through intermediate models—stopwatch games and updatable timed games—with explicit transformations and bisimulation proofs (via mappings such as $eta_1$ and $eta_2$ and state mappings like $v^*(x)=v(x)/\text{flow}(l,x)$). By translating ISR strategies to Timed Game strategies, the authors enable the use of existing timed-game realizability tools to synthesize winning strategies and then translate them back to the original hybrid setting. This chain of reductions yields decidability results for LTL objectives in ISR games and opens a path to extending these results to broader classes of initialized rectangular hybrid automata.
Abstract
Hybrid games are games played on a finite graph endowed with real variables which may model behaviors of discrete controllers of continuous systems. The synthesis problem for hybrid games is decidable for classical objectives (like LTL formulas) when the games are initialized singular, meaning that the slopes of the continuous variables are piecewise constant and variables are reset whenever their slope changes. The known proof adapts the region construction from timed games. In this paper we show that initialized singular games can be reduced, via a sequence of alternating bisimulations, to timed games, generalizing the known reductions by bisimulation from initialized singular automata to timed automata. Alternating bisimulation is the generalization of bisimulation to games, accomodating a strategy translation lemma by which, when two games are bisimilar and carry the same observations, each strategy in one of the games can be translated to a strategy in the second game such that all the outcomes of the second strategy satisfies the same property that are satisfied by the first strategy. The advantage of the proposed approach is that one may then use realizability tools for timed games to synthesize a winning strategy for a given objective, and then use the strategy translation lemma to obtain a winning strategy in the hybrid game for the same objective.