A Temporal Logic Specification Interface for Automata-Theoretic Finitary Control Synthesis

This paper presents a correct and complete algorithm that translates propositional linear time temporal logic (PTL) formulae to event-based automata for finitary control synthesis. It proposes the translation algorithm as a specification interface to well-established automata-theoretic control synthesis methods for discrete-event systems (DES’s). This allows control requirements to be more easily described and understood in an expressive and readable language that temporal logic is widely recognized as. Adding such a translation interface effectively combines specifiability and readability in temporal logic with prescriptiveness and computability in automata. The former temporal logic features support specification while the latter automata features support the prescription of DES dynamics and algorithmic computations. A practical implementation of the interface has been developed, providing an enabling technology for writing more readable control specifications in PTL that it translates for finitary control synthesis in automata. A simple example illustrates the use of the proposed temporal logic interface. Practical implications of the complexity of the translation algorithm are discussed.