IEEE Transactions on Automatic Control, Vol.56, No.12, 2986-2991, 2011
Bisimilarity Enforcement for Discrete Event Systems Using Deterministic Control
For discrete event systems, the control to enforce bisimilarity with respect to a given specification has been studied in [10], [12], [13]. In this note we consider the case when the control is required to be deterministic. While a deterministic control is restrictive compared to a nondeterministic one, the case of deterministic control has its own practical significance as it is easier to implement and computationally less expensive to verify. We provide a necessary and sufficient condition for the existence of a bisimilarity enforcing deterministic control, and discuss its computational complexity. We also study properties related to the synthesis of "subspecification" and "superspecification."