Controller Synthesis for Bisimulation Equivalence

Abstract

This thesis investigates the controller synthesis for bisimulation equivalence from both discrete and continuous aspects. From discrete perspective, supervisory control is studied to enforce bisimilarity for discrete event systems. Specifically, we consider three kinds of supervisory control problems: bisimilarity control, decentralized bisimilarity control and distributed bisimilarity control. For these problems, the existence conditions for bisimilarity/ decentralized bisimilarity/ distributed bisimilarity control are developed. When such existence conditions hold, we construct bisimilarity enforcing supervisors accordingly. Otherwise, the synthesis of achievable sub/sup-specifications is further investigated to enable bisimilarity/ decentralized bisimilarity/ distributed bisimilarity control. When it comes to continuous perspective, the control of multi-affine systems for bisimulation equivalence is presented. We partition the state space into rectangles, and then study the control of multi-affine systems on rectangles. Resorting to the proposed control method, a bisimilarly abstracted system is obtained. A fully automated procedure is then developed to control multi-affine systems for temporal logic specifications.