Automatica, Vol.50, No.1, 287-290, 2014
Bisimilarity enforcing supervisory control for deterministic specifications
This paper studies the supervisory control of nondeterministic discrete event systems to achieve a bisimulation equivalence between the controlled system and the deterministic specification. In particular, a necessary and sufficient condition is given for the existence of a bisimilarity enforcing supervisor, and a polynomial algorithm is developed to verify such a condition. When the existence condition holds, a bisimilarity enforcing supervisor is constructed. Otherwise, two methods are provided for synthesizing supremal feasible sub-specifications. (C) 2013 Elsevier Ltd. All rights reserved.