Bisimilarity Enforcing Supervisory Control for Deterministic Specifications

Yajuan Sun, Hai Lin, Ben M. Chen

This paper investigates the supervisory control of nondeterministic discrete event systems to enforce bisimilarity with respect to deterministic specifications. A notion of synchronous simulation-based controllability is introduced as a necessary and sufficient condition 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 supervisor achieving bisimulation equivalence is constructed. Furthermore, when the existence condition does not hold, two different methods are provided for synthesizing maximal permissive sub-specifications.

picture_as_pdf flag

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment