Control of nondeterministic discrete event systems for bisimulation equivalence

We study supervisory control for enforcing nondeterministic specifications. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified linearly in both system and specification states.