Supervisory control of discrete event systems with CTL* temporal logic specifications

Supervisory control problem of discrete event systems with temporal logic specifications is studied in this paper. The full branching time logic-CTL* is used for expressing specifications of discrete event systems. The control problem of CTL* is reduced to the decision problem of CTL*. A small model theorem for the control of CTL* is obtained. It is shown that the control problem of CTL* (resp., CTL) is complete for deterministic double (resp., single) exponential time. A sound and complete supervisor synthesis algorithm for the control of CTL* is provided. Special cases of the control of computation tree logic (CTL) and linear-time temporal logic (LTL) are also studied. The main contributions of the paper are summarized as follows: (i) For the first time a sound and complete supervisory synthesis algorithm for CTL* specifications has been obtained; (ii) Usage of temporal logic makes the specification specifying process easier and user-friendly since natural language specifications can be easily translated to temporal logic specifications (when compared to formal language/automata-based specifications) and at the same time there is no increase in the computational complexity (compared to that of formal language/automata-based specifications); (iii) CTL* temporal logic allows the control constraints on the sequences of states which can be also captured by a regular *-language or w-language, as well as on the more general branching structures of states which can not be captured by a regular *-languaae or w-language.