Mutually non-blocking supervisory control of discrete event systems

A single maximally permissive and nonblocking supervisor to simultaneously fulfill several marked specification languages pertaining to a single plant, is investigated. It is shown that a supervisor guaranteeing that the controlled system can execute traces within one specification while always being able to continue into the traces of the other does exist. Given a plant G and two marked specification languages K₁ and K₂, a supervisor S is said to be (K₁ , K₂)-mutually nonblocking if L_m(G||S)∩K_i⊆L¯_m ¯(¯G¯||¯S¯)¯∩¯K¯ _j¯ for i,j=1,2. 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. In this way the controlled system can execute traces within one specification while always being able to continue into the traces of the other and thus not blocking the other specification. We will show that 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 specification. There does exist a unique supremal such language. Furthermore, in the case that each specification language is nonconflicting with respect to the prefix-closure of the other, this supremal language can be calculated in a modular fashion, by expressing it as a union of the supremal prefix-bounded sub-languages of the respective specifications