Automatica, Vol.36, No.12, 1863-1869, 2000
Mutually nonblocking supervisory control of discrete event systems
A single maximally permissive and nonblocking supervisor to simultaneously fulfill several marked specifications pertaining to a single plant is investigated. Given a plant G and two marked specification languages K-1 and K-2, a supervisor S is said to be (K-1, K-2)-mutually nonblocking if (for i,j = 1,2) L-m(G parallel toS)boolean ANDK(i)subset of or equal toL(m)(G parallel toS)boolean ANDK(j). This means that when the closed-loop system marks a trace of K-i, then it is always able to continue to a trace of K-j, also marked in the closed-loop system. Thus, the controlled system can execute traces within one specification while always being able to continue a trace of the other and hence not blocking the other specification. A complete, globally nonblocking and (K-1, K-2)-mutually nonblocking supervisor such that L-m(G parallel toS)subset of or equal toK(1)boolean ORK2 exists if and only if there exists a controllable mutually nonblocking sublanguage of the union of the specifications. There does exist a supremal such language. Furthermore, in the case that each specification is nonconflicting with respect to the prefix-closure of the other, this supremal language can be calculated by expressing it as the union of the supremal prefix-bounded sublanguages of the respective specifications. Finally, we show that the multiply nonblocking supervision of Thistle, Malhame, Hoang and Lafortune ((1997). Internal Report, Dept, de genie electrique ct de genie informatique, Ecole Polytechnique de Montreal, Canada) is equivalent to globally and mutually nonblocking supervision.
Keywords:discrete event systems;supervisory control theory;formal languages;modular specification;mutually nonblocking languages;nonconflicting languages