Real-time control with parametric timed reachability games

Abstract: Timed game automata are used for solving control problems on real-time systems. A timed reachability game consists in finding a strategy for the controller for the system, modeled as a timed automaton. Such a controller says when and which of some "controllable " actions should be taken in order to reach "goal " states. We deal with a parametric version of timed game automata. We define parametric timed reachability games and introduce their subclass for which the existence of a parameter valuation, such that there is a strategy for the controller to reach the "goal " state, is decidable. We also propose a semi-algorithm to symbolically compute the corresponding set of parameter valuations