CONTROL OF DISCRETE EVENT SYSTEMS IN TEMPORAL LOGIC
Akash Deshpande, Pravin P. Varaiya · 1994
This paper presents two approaches to the control of a discrete event system (DES) - one semantic, the other syntactic - within the framework of Propositional Linear Temporal Logic (PLTL). Given the plant behavior and the desired behavior, both described in PLTL, a causal, nonblocking and fair controller is to be synthesized that restricts the system's closed loop behavior to a subset of the desired behavior. The syntactic procedure gives the maximal such controller; the semantic technique gives the synthesis of the controller.