切换系统可达集计算研究及其在非线性系统形式化验证中的应用

The dynamic behaviors of switched system are complex, the computation of reachable set of a switched system can quantitatively characterize the region of state trajectories produced by the complex dynamic behaviors of the switched system, which is of significant theoretical importance for the analysis of switched systems. On the other hand, the formal verification problem for nonlinear system is a difficult problem in the field of verification, switched linear systems can approximate nonlinear systems to some extent, thus it is promising and meaningful to employ reachable set estimation results of switched system to solve formal verification problems for nonlinear systems. The research of this project includes: 1. Propose an initial state and input sets dependent Lyapunov function approach for reachable set estimation of switched system, and make full use of the information of switching law to reduce the conservativeness of the computation results. 2. Use model reduction and system approximation techniques to reduce the computational complexities so that the reachable set estimation results can be extended to the cases with high dimensions and large number of subsystems. 3. Hybridize nonlinear system, and design the formal verification algorithm for nonlinear systems based on the reachable set computation of switched systems. 4. Create MATLAB toolboxes, and provide support for reachable set estimation of practical switched systems and for verification of practical nonlinear systems.

切换系统具有复杂的动态行为，切换系统可达集计算能够对切换系统复杂动态行为的状态轨迹范围进行定量的描述，对切换系统的性质分析具有重要的理论研究意义；另一方面，非线性系统的形式化验证问题一直以来都是系统验证研究领域的难题，线性切换系统能在某种程度上对非线性系统进行近似，因此切换系统可达集研究成果在解决非线性系统的形式化验证问题中具有很好的应用前景和实际意义。本项目的研究内容有：1、提出依赖初始状态集合与输入集合描述的Lyapunov函数方法来研究切换系统可达集计算问题，并将充分利用切换规则的信息来降低计算结果的保守性。2、本项目将基于模型降阶和系统近似的方法来降低算法的计算复杂度，将研究成果推广到高阶与多子系统情形。3、对非线性系统进行混杂化，在切换系统可达集计算研究基础上设计非线性系统形式化验证的算法。4、建立MATLAB工具箱，为实际切换系统可达集计算与非线性系统验证提供支持。

切换系统作为一类重要的混杂系统，其形式简洁并且能够良好地反映连续变量与离散变量之间的关系，从某种意义上来说是沟通线性系统和非线性系统之间的桥梁。切换系统可达集计算能够对切换系统复杂动态行为的状态轨迹运行范围进行定量的描述，对切换系统的性质分析具有重要的理论研究意义，同时对实际切换系统及非线性系统的设计与验证中也具有重要的实践指导意义。本项目的主要研究内容及取得的相关成果如下：1. 通过深入研究Lyapunov函数与不变集理论在切换系统的稳定性与可达集的应用，提出的方法能够大大降低现有的切换系统稳定和可达集分析结果。2. 提出了计算切换系统可达集的理论方法，并进一步研究了切换规则与可达集之间的联系，提出了时间依赖切换系统的优化算法来降低可达集计算的保守性，并推广到了随机Markovian跃变系统的稳定性分析与可达集计算中。3. 进一步改进可达集计算算法，增强其可扩展性来处理更高维及更多子系统的切换系统。创新性地提出了虚拟时钟的概念，能够大大增加可达集计算方法的可扩展性。通过Bisimulaton的方法来降低系统的维数，然后通过降维后的系统来提高算法的可扩展性。通过利用Simulation的信息及区间计算方法，来提高可达集计算扩展性。 4. 基于切换系统的可达集计算的研究成果，将切换系统的可达集计算方法推广到非线性的可达集计算中，用于非线性系统的形式化验证问题中。提出了将非线性系统转化为线性参数变化系统的方法，然后通过判定线性参数变化系统可达集计算设计形式化验证算法。设计了数据驱动动态模型的可达集计算及形式化验证算法。5. 本项目还专门研究了含智能控制器如神经网络控制器的动态系统的可达集计算，设计了神经网络控制系统的可达集计算方法。6. 最后，将以上的研究成果进一步总结归纳，设计切换系统与非线性系统的可达集计算与形式化验证的MATLAB工具箱。本项目的研究成果完善了现有的切换系统理论体系，并在复杂系统验证问题具有较为深刻的实际应用意义。研究成果能够进一步促进切换系统可达集计算与非线性系统形式化验证的理论与实践，丰富切换系统与形式化验证领域的研究成果，为实际系统的可达集计算与形式化验证软件设计提供关键的算法支持与解决方案。