Polynomial-time verification for bisimilarity control of partially observed nondeterministic discrete event systems with deterministic specifications

We consider a bisimilarity control problem for partially observed nondeterministic discrete event systems. It requires us to synthesize a supervisor that works under partial observation so that the supervised system is bisimilar to the specification. The computational complexity of verifying the known necessary and sufficient condition for the existence of such a supervisor is exponential in the numbers of states of the system and the specification. We show that, in a special case where the specification is deterministic, the existence of a supervisor that solves the bisimilarity control problem is polynomially verified.(c) 2023 Elsevier Ltd. All rights reserved.