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.