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.

翻译：混合博弈是在一个配备实变量的有限图上进行的博弈，这些实变量可用于建模连续系统的离散控制器的行为。当博弈是初始奇异时，即连续变量的斜率是分段常数且变量在其斜率改变时被重置，混合博弈对于经典目标（如LTL公式）的合成问题是可判定的。已知的证明方法借鉴了时间博弈的区域构造。本文证明，初始奇异博弈可以通过一系列交替互模拟约简为时间博弈，从而推广了从初始奇异自动机到时间自动机的已知互模拟约简。交替互模拟是互模拟在博弈中的推广，它适应了一个策略转换引理：当两个博弈互模拟且具有相同的观测时，其中一个博弈中的每个策略都可以转换为第二个博弈中的一个策略，使得第二个策略的所有结果都满足第一个策略所满足的相同性质。所提方法的优势在于，随后可以利用时间博弈的可实现性工具来为给定目标合成一个获胜策略，然后利用策略转换引理在混合博弈中获得同一目标的获胜策略。