Logical time control of concurrent DES

The synthesis of controllers for reactive systems can be done by computing winning strategies in two-player games. Timed (game) Automata are an appropriate formalism to model real-time embedded systems but are not easy to use for controller synthesis for two reasons: i) timed models require the knowledge of the precise timings of the system; for example, if an action must occur in the future, the deadline of this occurrence must be known, ii) in practice, the dense state space makes the computation of the controller often impossible for complex systems. This paper introduces an extension of untimed game automata with logical time. The new semantics introduces two new types of uncontrollable actions: delayed actions which are possibly avoidable, and ineluctable actions which will eventually happen if nothing is done to abort it. The controller synthesis problem is adapted to this new semantics. This paper focuses specifically on the reachability and safety objectives and gives algorithms to generate a controller. The paper then extends these results to Game Petri Nets which can express concurrent timed behaviors and where an avoidable transition can lose its avoidability by the elapsing of time. The usefulness of this new model is illustrated by a real device driver synthesis example.