Supervisory Control of Fair Discrete-Event Systems: A Canonical Temporal Logic Foundation

Abstract

This paper studies the linear-time temporal logic (LTL) control of a class of fair discrete-event systems (DESs). It is motivated by the curious extent in which the use of LTL can be strengthened and differentiated in control theory development. Over a fair DES model, a marker-progressive supervisory control problem is formulated in LTL. The problem formulation admits a more flexible specification of multiple markers to distinguish different DES tasks, and seeks to find a supervisor-a passive control function by convention for specified temporal safety-such that a fair DES under its control is guaranteed to make constant progress to these markers. The problem is studied in terms of DES marker-controllability-a new controllability concept formulation of temporal safety for constant marker progress. This new formulation sheds light on how event fairness in DESs coachieves such marker progress with supervision that exists. It is shown that a solution supervisor may be found by canonical LTL verification. Three examples are provided for illustration.