Bisimilarity Control under Partial Observation of Deterministic Discrete Event Systems

The complexity of the general bisimilarity control problem under partial observation is doubly exponential in the product of the plant and the specification sizes [7]. In order to identify a special case where the complexity may be more manageable, we restrict attention to the class of deterministic plants. In this case, the complexity of verifying existence of a controller turns out to be polynomial, whereas that of performing its synthesis is singly exponential. We establish state-controllability (SC) together with state-recognizability (SR) as a necessary and sufficient condition for the existence of a control. The notion of SC was introduced in [8] as an existence condition for the same problem under the restriction of complete observability of events; and it generalizes the notion of language-controllability (LC) from the setting of language-control to bisimilarity-control. In the presence of partial observation, a supervisor is required to be observation-compatible (also called M-compatible), and the additional condition of SR is needed for the existence of such a supervisor. The property of SR is same as bisimilarity with such a system that can be transformed by state-mergers to a M-compatible system, without altering the bisimilarity of the control it exercises. SR generalizes the notion of language-recognizability [1] in a similar manner as SC generalizes LC. We show that SR is polynomially verifiable, and also present an exponential complexity algorithm for synthesizing of a bisimilarity enforcing Supervisor.