화학공학소재연구정보센터
IEEE Transactions on Automatic Control, Vol.55, No.11, 2527-2541, 2010
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.