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 systems of industrial size. Owing to the high computational complexity, synthesizing a nonblocking supervisor for a large scale system is never easy, if still possible. In this paper we attempt to solve this synthesis problem by using abstractions. We first introduce a new abstraction operation, which preserves the nonblocking property. Then we describe how to synthesize supervisors by using abstractions of relevant automata so that the high computational complexity associated with the synchronous product described in the Ramadge-Wonham supervisory control theory (SCT) may be avoided.