Model abstraction of nondeterministic finite-state automata in supervisor synthesis

Blockingness is one of the major obstacles that need to be overcome in the Ramadge-Wonham supervisory synthesis paradigm, especially for large systems. In this paper we propose an abstraction technique to overcome this difficulty. We first provide details of this abstraction technique, then describe how it can be applied to a supervisor synthesis problem, where plant models are nondeterministic but specifications and supervisors are deterministic. We show that a nonblocking supervisor for an abstraction of a plant under a specification is guaranteed to be a nonblocking supervisor of the original plant under the same specification. The reverse statement is also true, if we impose an additional constraint in the choice of the alphabet of abstraction, i.e. every event, which is either observable or labels a transition to a marker state, is contained in the alphabet of abstraction.