Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data-Driven Approach

• 成果类型: Article
• 署名作者: Nejati, Ameneh; Lavaei, Abolfazl; Jagtap, Pushpak; Soudjani, Sadegh; Zamani, Majid
• 署名单位: Technical University of Munich; University of Munich; Newcastle University - UK; Bosch; Indian Institute of Science (IISC) - Bangalore; University of Colorado System; University of Colorado Boulder
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2023.3255141
• 发表日期: 2023
• 页码: 3011-3024
• 关键词: safety; trajectory; Probabilistic logic; computational modeling; mathematical models; Upper bound; optimization; Data-driven barrier certificates; discrete-time and continuous-time systems; formal safety verification; robust convex program; scenario convex program

摘要

This article is concerned with a formal verification scheme for both discrete- and continuous-time deterministic systems with unknown mathematical models. The main target is to verify the safety of unknown systems based on the construction of barrier certificates via a set of data collected from trajectories of systems while providing an a-priori guaranteed confidence on the safety. In our proposed framework, we first cast the original safety problem as a robust convex program (RCP). Solving the proposed RCP is not tractable in general since the unknown model appears in one of the constraints. Instead, we collect finite numbers of data from trajectories of the system and provide a scenario convex program (SCP) corresponding to the original RCP. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP, and as a result, we formally quantify the safety guarantee of unknown systems based on the number of data points and a required level of confidence. We propose our framework in both discrete-time and continuous-time settings. We illustrate the effectiveness of our proposed results by first applying them to an unknown continuous-time room temperature system. We verify that the temperature of the room maintains in a comfort zone with some desirable confidence by collecting data from trajectories of the system. To show the applicability of our techniques to higher dimensional systems with nonlinear dynamics, we then apply our results to a continuous-time nonlinear jet engine compressor and a discrete-time DC motor.