Trigger-Based Discretization of Hybrid Games for Autonomous Cyber-Physical Systems

Hybrid games are a powerful framework for modelling interactions between cyber-physical systems (CPS). While their high level of nondeterminism allows the modelling of complex systems, it also makes many properties undecidable. This paper presents Hybrid Games with Triggers (HGT), an extension that reduces nondeterminism by embedding agents' rational decision-making as triggers -conditions that, when met, prompt the agents to act. This approach leads to a time-abstract discrete game with a countable state space, where an agent has a winning strategy in the discrete game if and only if they do in the HGT. Our discretisation preserves both the continuous and discrete dynamics of the original hybrid game, providing a more structured, analysable model without sacrificing dynamic expressivity.