Title :
Supervisory control of discrete event systems with CTL* temporal logic specifications
Author :
Jiang, Shengbing ; Kumar, Ratnesh
Author_Institution :
Dept. of Electr. & Comput. Eng., Kentucky Univ., Lexington, KY, USA
Abstract :
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 ω-language, as well as on the more general branching structures of states which can not be captured by a regular *-language or ω-language
Keywords :
control system synthesis; discrete event systems; formal languages; temporal logic; ω-language; CTL* temporal logic specifications; computation tree logic; deterministic double exponential time; discrete event systems; full branching time logic; linear-time temporal logic; natural language specifications; regular *-language; supervisor synthesis algorithm; supervisory control; Automatic control; Computational complexity; Control systems; Discrete event systems; Distributed control; Formal languages; Logic design; Natural languages; Strain control; Supervisory control;
Conference_Titel :
Decision and Control, 2001. Proceedings of the 40th IEEE Conference on
Conference_Location :
Orlando, FL
Print_ISBN :
0-7803-7061-9
DOI :
10.1109/.2001.980826