A Metric Temporal Logic Specification Interface for Real-Time Discrete-Event Control

In supervisory control of timed discrete-event systems (TDESs), a conceptually well founded finitary control synthesis framework is developed, and it requires specifications to be prescribed as finite (-trace) automata in the form of timed transition graphs (TTGs). However, prescribing real-time specifications as TTGs is a nontrivial task that must be resolved before the formal framework could expect to become widely used. In addressing this specification problem, metric temporal logic (MTL) is proposed in this paper as a control specification language for use with the TTG-based control synthesis framework. MTL is a designer-friendly formalism due to its human or natural language expressiveness and readability, and is well suited for specifying real-time control specifications. In automating TTG prescription, this paper proposes an MTL interface to the control synthesis framework. The interface is proved to be a correct and complete translation algorithm that converts finitary control specifications written in state-based MTL formulas for a given TDES model into deterministic finite TTGs. Integrated, the MTL interface and the control synthesis framework combine the human expressiveness and readability of MTL with the algorithmic computability of TTGs, and together provide a new and convenient MTL specification-based design tool for automated prescription of TTGs and real-time control synthesis. Illustrative examples demonstrate the utility of the MTL interface.