A two-pass algorithm for compositional synthesis of modular supervisors for largescale
systems of composed finite-state automata is proposed. The first pass provides
an efficient method to determine whether a supervisory control problem has a
solution, without explicitly constructing the synchronous composition of all components.
If a solution exists, the second pass yields an over-approximation of the
least restrictive solution which, if nonblocking, is a modular representation of the
least restrictive supervisor. Using a new type of equivalence of nondeterministic
processes, called synthesis equivalence, a wide range of abstractions can be employed
to mitigate state-space explosion throughout the algorithm.
