Automatic synthesis of a subclass of schedulers in timed systems

AbstractIn this article we present a synthesis technique for generating schedulers for real-time systems. The aim of the scheduler is to ensure (via restricting the general behaviour) that the real-time system satisfies the specification. The real-time system and the specification are described as Alur–Dill timed automata while the synthesised scheduler is a type of timed trajectory automaton. This allows us to perform the synthesis without incurring the cost of constructing timed regions. We also note a simple constraint that the specification has to satisfy for this technique to be useful