Timed Games Under Environmental Interference with Real-Time Objectives

Classical Timed Games formulations may be unsuitable, or require substantial modeling effort, to capture complex interaction patterns between a controller and its surrounding environment, in which the non-determinism must be resolved after the controller has chosen which action to perform. This paper introduces Timed CLTLoc Games (TCGs), a novel Timed Game variant designed to facilitate the modeling of such patterns. Unlike classical Timed Games, TCGs partition locations rather than actions, and use Constraint Linear Temporal Logic over clocks formulae to specify the controller’s objectives. We implement algorithms for solving TCGs in our C++20 region-based library Tarzan, leveraging OpenMP for efficient parallelization. We then validate our theoretical results through an empirical evaluation on a Production Cell case study, demonstrating that the region-based implementation is computationally efficient in practice for medium-sized models.