On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, Jaco van de Pol
TL;DR
This work tackles parameter synthesis for reachability in Parametric Timed Games by extending the On-The-Fly (OTF) approach to the PTG setting. It introduces a symbolic, zone-based representation via the Parametric Zone Graph and leverages three core operators—$ ext{WinningMoves}$, $ ext{Uncontrollable}$, and $ ext{SafePred}$—to compute a fixed-point characterization of winning states. The authors implement the PTG synthesis within the Imitator framework, augmenting it with pruning techniques such as coverage pruning, inclusion checking, and cumulative pruning, and evaluate on large case studies including the Bounded Retransmission Protocol and Production Cell. While the problem is undecidable in general and the semi-algorithm may not terminate, the results establish soundness and limit-completeness, with practical improvements in termination and performance observed under the proposed optimizations.
Abstract
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations ``in the limit''.