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₁ and K₂, a supervisor S is said to be (K₁,K₂)-mutually nonblocking if (for i,j=1,2)

Full-size image

. 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₁,K₂)-mutually nonblocking supervisor such that L_m(G || S)K₁K₂ 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 et de genie informatique, Ecole Polytechnique de Montreal, Canada) is equivalent to globally and mutually nonblocking supervision.