  This paper investigates the supervisory control of nondeterministic discrete
event systems to enforce bisimilarity with respect to deterministic
specifications. A notion of synchronous simulation-based controllability is
introduced as a necessary and sufficient condition for the existence of a
bisimilarity enforcing supervisor, and a polynomial algorithm is developed to
verify such a condition. When the existence condition holds, a supervisor
achieving bisimulation equivalence is constructed. Furthermore, when the
existence condition does not hold, two different methods are provided for
synthesizing maximal permissive sub-specifications.
