Synthesizing controllers from real-time specifications

We present an algorithm for synthesizing real-time controllers specified in a subset of the interval temporal logic duration calculus. The synthesized controllers are given in terms of programmable logic controller (PLC)-automata, which are an abstract description of programs of polling machines. PLC-automata can be implemented directly on PLCs, a special kind of polling real-time controllers that are often used in industry to control production cells and batch processes. We prove the correctness of the algorithm by the duration calculus semantics for PLC-automata. Furthermore, the set of specifications on which the algorithm terminates with a well-formed PLC-automaton coincides with the set of specifications that are implementable in principle. Hence, the algorithm also decides whether a specification given in this subset of the duration calculus is implementable. We demonstrate the behavior of the algorithm by an example and apply the algorithm to the well-known “gasburner” case study