Bisimilarity enforcing supervisory control of nondeterministic discrete event systems

In this paper, we investigate the supervisory control of discrete event systems for bisimulation equivalence, in which the plant and the specification are modeled as nondeterministic automata. A notion of synchronous simulation-based state controllability is introduced and is shown to be a sufficient condition for the existence of a bisimilarity enforcing supervisor. A polynomial algorithm is developed to check such a condition. When the existence condition holds, a bisimilarity enforcing supervisor is constructed. When the condition does not hold, the synthesis of feasible sub-specifications is further studied.