Decentralized bisimilarity control of discrete event systems

This paper studies the decentralized control of discrete event systems (DESs) for bisimulation equivalence, where the plant and the specification are taken to be nondeterministic and the supervisor is taken to be deterministic. An automaton-based control framework is formalized, upon which we develop two architectures-a conjunctive architecture and a disjunctive architecture with respect to different decision making rules for the decentralized bisimilarity control. Under these architectures, necessary and sufficient conditions for the existence of decentralized bisimilarity supervisors are derived respectively, which extend traditional results of supervisory control from language equivalence to bisimulation equivalence. It is shown that these conditions can be verified with exponential complexity. Furthermore, the synthesis of decentralized bisimilarity supervisors is further presented when the existence condition holds.