Control of Nondeterministic Discrete Event Systems for Simulation Equivalence

This paper studies supervisory control of discrete event systems subject to specifications modeled as nondeterministic automata. The control is exercised so that the controlled system is simulation equivalent to the (nondeterministic) specification. Properties expressed in the universal fragment of the branching-time logic can equivalently be expressed as simulation equivalence specifications. This makes the simulation equivalence a natural choice for behavioral equivalence in many applications and it has found wide applicability in abstraction-based approaches to verification. While simulation equivalence is more general than language equivalence, we show that existence as well as synthesis of both the target and range control problems remain polynomially solvable. Our development shows that the simulation relation is a preorder over automata, with the union and the synchronization of the automata serving as an infimal upperbound and a supremal lowerbound, respectively. For the special case when the plant is deterministic, the notion of state-controllable-similar is introduced as a necessary and sufficient condition for the existence of similarity enforcing supervisor. We also present conditions for the existence of a similarity enforcing supervisor that is deterministic.