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

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.

Automated summary

This paper explores the use of linear-time temporal logic (LTL) for controlling a class of fair discrete-event systems (DESs) and introduces a new concept of DES marker-controllability to describe constant marker progress, shedding light on the coordination between event fairness and supervision in DESs. The study shows that a solution supervisor can be found through canonical LTL verification and provides three examples for illustration.