IEEE Transactions on Automatic Control, Vol.47, No.10, 1779-1783, 2002
Existence characterizations of temporal-safety supervisors
This note shows that beyond the expected basic results on supervisor existence and synthesis, the temporal logic systems analysis for the invariance control of an arbitrary past formula P yields new insights into supremal control of temporal safety. These insights come in the form of equivalent temporal characterizations. One characterization allows a natural-language interpretation which provides a very good intuitive feel of the supremal controllability concept. Another provides a structurally elegant representation revealing that the past formula P must never be stronger than some fixed logic "constant" Importantly, from the control synthesis viewpoint, these temporal characterizations provide the opportunity to use several (industrial-strength) commercially available theorem provers to accomplish the synthesis task in a transparent fashion. Finally a controllable canonical form-unifying the supremal, exact, and infimal existences of temporal-safety control-is exhibited and its theoretical significance is discussed.
Keywords:controllable canonical form;logical discrete-event (DES) system;supervisory control;temporal safety