Control of nondeterministic discrete event systems for simulation equivalence

The paper studies supervisory control of discrete event systems when specification is nondeterministic and modeled as a nondeterministic state machine. The control is exercised so that the controlled plant is simulation equivalent to the (nondeterministic) specification. In our previous work on nondeterministic specification [C. Zhou et al., 2004], the requirement of bisimulation equivalence between the controlled plant and the specification was studied. Simulation equivalence is weaker than bisimulation equivalence but stronger than language equivalence: Besides the language equality, simulation equivalence specifies an upper bound for the branching behavior following any trace, whereas bisimulation equivalence specifies the exact branching behavior following any trace. Simulation equivalence preserves ∀CTL temporal logic specifications, which is more general than LTL (preserved under language equivalence) but less general than CTL (preserved under bisimulation equivalence). We develop necessary and sufficient conditions for the existence of a supervisor and provide polynomial complexity algorithms for testing the existence and synthesis of a supervisor. For the special case when plant is deterministic, the notion of state-controllable-similar is introduced as a necessary and sufficient condition for the existence of similarity enforcing supervisor.