基于矩方法的混成系统可达集计算方法及其应用

Reachable set computation is one of the main approaches to safety verification of hybrid systems. Existing computation methods rely on gridding of the state and time space, thus suffering from huge computational costs and inflated computational errors. The proposed project studies the reachable set computation problem from a new view point of measures and moments, which exploits the moment method to describe reachable set globally rather than via trajectories, and thus can improve the efficiency and precision of existing methods. To achieve this, the proposed project plans to investigate moment-based reachable set computation method for hybrid systems and its extension to uncertain and stochastic hybrid systems, the highly efficient solving algorithms for related large-scale SDP problems, as well as applications of the proposed method to automated driving systems. By defining what so called transition measure and full generator we extend moment-based reachable computation methods to hybrid systems and stochastic hybrid systems. By analyzing the specific properties of SDP problems arising in reachable set computation we design new SDP solving algorithms with high efficiency. The ultimate goal of this project is to give a new reachable set computation method with high scalability and applicability, and carry out fruitful practical applications on the case of an Adaptive Cruise Control (ACC) system. The research conducted in this project will strongly advance the development of the hybrid system verification area, and will be of great significance for enhancing the trustworthiness of safety-critical embedded control systems.

可达集计算是混成系统安全性验证的主要方法之一。现有混成系统可达集计算基于状态和时间划分，存在时空开销大且结果误差膨胀的问题。本项目从测度和矩的全新观点、利用矩方法的全局性从整体上刻画可达集，避免对时空的划分，有望提升混成系统可达集计算效率、精度和适用范围。为此，拟开展基于测度和矩方法的混成系统可达集计算方法研究、结合矩方法特性的大规模半定规划（SDP）问题高效求解算法研究、基于矩方法的概率随机混成系统可达集计算方法研究以及在自动驾驶等领域的安全性验证实例研究。通过定义混成系统迁移测度及完全生成元实现矩方法在混成和随机混成系统中的扩展，通过分析可达集计算场景下SDP问题的特性改进其求解效率，给出一种高效、精确、适用范围广的混成系统可达集计算新方法，并针对自适应巡航控制系统开展富有成效的实际应用。本项目的研究将有力推动混成系统形式化验证发展，对保障安全攸关嵌入式控制系统的可信性有重要意义。

混成系统作为实际信息物理系统的重要数学模型，其安全性验证问题对安全攸关系统具有重要意义。含神经网络组件的混成/连续系统是伴随着项目执行期发展起来的一类更特殊、更复杂、更具有前瞻性的混成系统模型，本项目重点研究该类系统的验证问题。障碍函数是描述系统可达集上界一类有效方法，该方法有效避免可达集计算方法基于状态和时间划分，存在时空开销大且结果误差膨胀的问题。然而，障碍函数的存在性作为系统安全性形式化保障的充分条件，如何有效生成障碍函数是当前混成系统验证方法的关键研究问题。对此，本项目深入探索障碍函数有效生成方法，针对混成/连续系统安全性，研究了有别于传统多项式型障碍函数生成的全新障碍函数有效生成方法；同时，借助于障碍函数生成方法研究系统安全控制器生成方法；研究了面向障碍函数生成问题的半定规划问题高效求解算法；研究了更具一般性的概率随机混成/连续系统安全验证；结合以上成果，研究了不同应用领域的安全验证以及安全控制案例。具体地，本项目1）首次提出了一类新的神经网络型障碍函数生成方法，相关研究成果能有效处理更多传统多项式型障碍函数无法解决的系统验证问题；2）提出了神经网络形式的安全控制器生成方法，为智能方法应用于安全控制研究提出了新的可能性；3）提出了面向控制器具有随机性的概率系统安全验证方法，该研究成果为进一步研究更具一般性的随机系统奠定基础；4）开展了安全性验证和控制生成实例研究，包括小车智能控制案例研究、工业油泵智能控制研究、飞行避障控制和安全验证案例研究，这些案例研究为研究成果的应用和推广提供了契机。研究期间，共发表学术论文9篇，其中包括国际会议CAV2021、AAAI2023（已接收）、HSCC2020，国际学术期刊FAoC，国内软件领域重要期刊《软件学报》。本项目的研究结合传统形式化方法和智能学习技术为复杂的智能系统验证研究奠定了基础。