基于计算实代数几何的混成系统验证研究

Hybrid systems are dynamical systems governed by interacting discrete and continuous dynamics. They are widely used to modelling safety-critical systems, where a number of computational components are deployed in a physical environment. Hybrid systems give rise to emergent behaviors that limit the efficiency and scalability of the existing verification methods for hybrid systems. To face the complexity, we will mainly focus on the study of the following problems. The project aims to build a novel method based on computational algebraic geometry to attack the the non-convex problem of bilinear programming solving, derived from the problem of barrier certification generation, which enhances the capability of barrier certificate based approaches. We develop a property directed incremental method for generating inductive invariants of nonlinear hybrid systems, to improve the scalability. We also apply a martingale analysis based method to verify qualitative and quantitative properties of stochastic hybrid systems. In order to validate the developed methods and techniques, we apply them to verify the safety of several safety-critical systems, such as air traffic control systems and train control systems. Through fulfilling the project, the research results will provide a powerful support for quality assuring of complex hybrid systems.

混成系统是一类既有连续变化又有离散变化，且连续变化与离散变化相互交织相互作用的系统。它被广泛应用于攸关安全系统的建模。混成系统的验证技术是保证安全攸关系统满足安全性等重要性质的有效手段。混成系统先天的复杂性，使得已有验证技术在可处理问题的种类，计算效率和可扩展性上有很大的不足。本项目围绕混成系统验证研究中障碍函数生成、不变式生成和随机混成系统的定性与定量验证三个关键问题展开研究工作，以设计新的计算方法为突破口，研究基于计算实代数几何的非凸双线性规划的求解方法，以提高障碍函数生成技术可处理问题的能力，提升计算效率；研究属性制导的不变式增量生成方法，通过有效的状态空间缩减，提高验证技术的可扩展性；研究基于鞅分析的随机混成系统验证方法，以支持随机混成系统安全性的定量分析与定性判定。以空中交通管制系统和列车控制系统等基准系统为对象，展开实例研究。最终为复杂混成系统验证提供理论、方法和工具支撑。

混成系统是一类既有连续变化又有离散变化，且连续变化与离散变化相互交织相互作用的系统。它被广泛应用于安全攸关系统的建模,例如交通控制系统，自动驾驶系统等。混成系统的验证技术是保证安全攸关系统满足安全性等重要性质的有效手段。混成系统先天的复杂性，使得已有验证技术在可处理问题的种类、计算效率和可扩展性上有很大的不足。本项目具体取得以下研究成果：.1）基于计算实代数几何方法计算半代数系统的可验证实数解，相比于其他方法求解速度更快，更能处理大规模问题的求解，同时为了解决浮点计算产生数值误差问题，采用基于区间分析的验证方法。.2）提出了基于双线性矩阵不等式求解以及双线性规划求解生成障碍函数来验证确定混成系统安全性质的方法。本报告给出了两种新的计算方法，理论分析与大量实验表明该方法比主流的SOS松弛方法具有更低的计算复杂度。.3）基于概率障碍函数生成方法验证随机混成系统。针对随机混成系统，给出了一种新的计算方法来生成概率障碍函数，以获得系统的安全性质的概率下界。理论分析以及大量实验结果表明，所提方法具有多项式时间的复杂度，能有效给出随机混成系统的安全性概率下界。.4) 含有AI组件系统的安全验证以及AI组件的设计与构造。针对含有AI组件的系统，本项目提出了基于多项式抽象以及非线性约束求解的方法来验证系统无限时间的安全性。针对系统预先给定的安全需求，我们提出了一种安全的强化学习方法来构造深度神经网络的控制器。与主流的强化学习方法相比，该方法具有较低的计算复杂度。