Control of Nondeterministic Systems for Bisimulation Equivalence Under Partial Information

In this article, we investigate the synthesis of a (possibly nondeterministic) supervisor, with partial information, such that the controlled nondeterministic plant is bisimulation equivalent to a nondeterministic specification. We derive a new necessary and sufficient condition for the existence of a supervisor and provide an algorithm for the supervisor construction when one exists. The algorithm is exponential in the size of the plant and specification, a substantial improvement over the double exponential cost from exhaustive search. We show that the cases of complete information and deterministic control are special cases of the presented theory.