Formal Control Synthesis via Simulation Relations and Behavioral Theory for Discrete-Time Descriptor Systems

• 成果类型: Article
• 署名作者: Haesaert, Sofie; Chen, Fei; Abate, Alessandro; Weiland, Siep
• 署名单位: Eindhoven University of Technology; Royal Institute of Technology; University of Oxford
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2020.2992443
• 发表日期: 2021
• 页码: 1024-1039
• 关键词: Mathematical model; dynamical systems; trajectory; control design; Couplings; Aerospace electronics; Approximate simulation relations; behavioral theory; descriptor systems (DS); formal verification

摘要

The control and verification of industrial processes, modeled as discrete-time descriptor systems, is often computationally hard due to the presence of both algebraic couplings and difference equations. In this article, we introduce a new control synthesis method for descriptor systems which is based on formal abstractions and enables control design over related reduced-order models. We leverage notions of exact and approximate similarity relations, which hold for the algebraic couplings that are inherent to descriptor systems. Using the behavioral framework, we extend a control refinement scheme for classical dynamical systems and develop a corresponding notion for descriptor systems: We show that any given well-posed controller of the abstract (reduced-order) descriptor system can be refined to a controller for the original descriptor system. The resulting controlled system preserves the same controlled output behavior in the case of exact similarity, whereas in the case of approximate similarity, the output behavior of the controlled descriptor system is shown to have a bounded deviation from that of the abstract model where the controller is designed.