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 CTL* 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 intimal 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. Note to Practitioners: Abstraction or unmodeled-dynamics can lead to nondeterminism that causes a system to transition to one of many states when certain events occur at certain states. For nondeterministic systems, specifying the usual state-sequencing constraints may not be adequate and state-branching constraints may also need to be specified such as: All paths contain a state starting from where all future states satisfy a certain property. Such a property is not expressible as language equivalence, but can be expressed using more general simulation equivalence. Simulation equivalence can specify all state-sequencing properties and the universal state-branching properties. The present paper studies the control of a (nondeterministic) system so that the controlled system satisfies a simulation equivalence specification. A main contribution is to show that as is the case with language, equivalence specifications, the control problem can be solved polynomially. Specializations to deterministic systems and deterministic controls are also considered.