A Method for the Automatic Derivation of Controllers Handling Real-Time Requirements

This paper describes a synthesis method that automatically derives controllers for timed discrete-event systems modeled by timed transition graphs and control requirements expressed by MTL (Metric Temporal Logic) formulas. Controllers are represented by Buchi automata and feedback functions. Synthesis is performed using standard forward-chaining search that evaluates the satisfiability of MTL formulas over sequences of states generated by occurrences of events and a control-directed backtracking technique. This method has several interesting features. First, it handles the issues of controllability, safety, liveness, and real time in a single framework. Second, it provides for generating controllers on-line, that is, the synthesis process can be stopped at any moment giving an approximate, but useful, result. Third, it does not require explicit storage of a timed transition graph over which formulas are checked, since it is incremental. Finally, it provides a solution in the form of an..