On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)

TL;DR

This paper presents an on-the-fly algorithm for synthesizing parameters in Parametric Timed Games, enabling verification of real-time systems with adjustable parameters, with heuristics to improve efficiency and a semi-algorithm that guarantees correctness in the limit.

Contribution

It adapts and implements an on-the-fly algorithm for parameter synthesis in PTGs, introducing heuristics and analyzing correctness despite undecidability.

Findings

Algorithm is feasible on large case studies.

Heuristics improve termination and speed.

Semi-algorithm produces correct valuations in the limit.

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''.