Bisimilarity Enforcing Supervisory Control for Deterministic Specifications
Systems and Control
2012-03-09 v1
Abstract
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.
Cite
@article{arxiv.1203.1745,
title = {Bisimilarity Enforcing Supervisory Control for Deterministic Specifications},
author = {Yajuan Sun and Hai Lin and Ben M. Chen},
journal= {arXiv preprint arXiv:1203.1745},
year = {2012}
}