时滞动力系统及混成系统的形式化验证

In real world, time-delays exist ubiquitously in systems in physics, biology and control, among others, namely, the evolution of the system depends not only on the current state, but also on past states. Delay differential equations are the popular mathematical model in characterizing the continuous dynamics of systems with delays. The study on formal verification of nonlinear delayed (hybrid) dynamical systems faces a large amount of challenges, and thus is still in infancy. This project is motivated by practical requirements in safety verification of delayed (hybrid) dynamical systems and centers the key scientific problems on reachability analysis of nonlinear delayed (hybrid) dynamical systems, for which the continuous dynamics are characterized by delay differential equations. The project aims to make progress in three aspects. First, we are trying to address several fundamental problems in the theory of formal verification of delayed (hybrid) dynamical systems, such as the investigation on properties of the solution to delay differential equations and the construction of (Hamilton-Jacobi) partial differential equations characterizing reachable sets of delay differential equations. Second, we aim at proposing scalable and efficient reachability analysis algorithms for nonlinear delayed (hybrid) dynamical systems. Finally, the newly designed algorithms will be implemented and integrated into our previous tools and further applied to the analysis and verification of real systems with delays such as high-speed trains. The application team features great interdisciplinarity and has been cooperating well for a long time. We believe that we would make progress in the research of the aforementioned problems in the theory and method of formal verification of nonlinear delayed (hybrid) dynamical systems, and facilitate the verification and analysis on real dynamical systems with delays such as high-speed trains.

在现实世界中，许多物理、生物、控制等实际系统中存在时滞现象，即系统的演化规律不仅依赖于当前的状态，还依赖于过去某些时刻的状态。时滞微分方程是常用于刻画这些系统连续动态行为的数学模型。非线性（混成）时滞系统形式化验证的研究尚处于初级探索阶段，其发展面临诸多挑战。本项目将从非线性（混成）时滞系统安全性验证的实际需求出发，围绕基于非线性时滞微分方程的（混成）时滞动力系统可达性分析问题，拟展开三方面的研究：一，非线性（混成）时滞系统形式化验证理论，包括时滞微分方程解性质的剖析及可达集的（Hamilton-Jacobi）偏微分方程刻画；二，大规模非线性（混成）时滞系统的可达性分析；三，相关工具开发及高铁等典型时滞系统的案例研究。我们的申请团队有很好的研究基础和多年卓有成效的合作，可望在非线性时滞（混成）系统形式化验证理论和方法的研究中取得突破，并将新的理论方法应用于高铁等典型时滞系统的验证和分析中。

时滞现象广泛地存在各种实际系统中, 如生物系统和自动化系统，这些系统的演化规律不仅依赖于当前的状态，还依赖于过去某些时刻的状态。在一些安全攸关系统中，时滞现象会使系统的安全性能下降，甚至导致系统不安全。时滞微分方程是刻画这些系统连续动态行为的主要数学模型，其可达集的上、下近似（可达集的超集、子集）计算是验证这些系统安全的主要手段之一。此项目研究时滞微分方程可达集计算的基础理论，提出可达集计算的有效方法。本项目取得了以下三方面的重要成果：1. 基于严格的数学推导得到了扰动时滞微分方程解满足同胚性质的充分条件，进而提出了计算此类时滞微分方程可达集上、下近似的边界方法，形成原型工具两套。 此方法只需计算边界的可达集，无需计算内点可达集，可极大的提高可达集计算效率及精度；2. 提出了刻画时滞微分方程无界时间可达-规避集合下近似的凸约束。据我们所知，这是首个刻画时滞微分方程可达-规避集合下近似的凸约束；3. 提出了基于数据驱动的可能近似正确检验方法，此方法可以计算现有基于数学模型的可达集计算方法无力处理的大规模复杂系统的可达集。此外，还提出了针对指数稳定时滞微分方程可达集上近似的计算方法以及混成时滞系统的安全控制律生成方法。. . 研究成果发表在控制理论及形式化方法的权威期刊及会议上，如IEEE Transactions on Automatic Control、SIAM Journal on Control and Optimization、IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems、CDC、ACC、IFAC、CAV 、HSCC 等，培养了两名博士生、两名硕士生。