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

A supervisory control problem of discrete event systems with temporal logic specifications is studied. 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 and at the same time there is no increase in the computational complexity ; (iii) CTL* temporal logic allows the control constraints on the sequences of states which can be also captured by a regular *-language or /spl omega/-language, as well as on the more general branching structures of states which can not be captured by a regular *-language or /spl omega/-language.