混成系统是一类复杂的动力系统,既包含连续动态系统,又包含离散事件系统,且两者之间相互作用。混成系统中连续变量和离散事件间的相互作用,使得混成系统的安全性验证非常困难。障碍函数生成的方法避免了复杂的可达集计算,在混成系统的分析与验证研究中得到了广泛应用。本文旨在研究基于迭代学习的障碍函数生成方法,以验证混成系统的安全性,主要研究内容如下:·研究了基于反例制导的障碍函数生成问题。本文采用反例制导归纳合成的思想,以Learner组件和Verifier组件交互合成障碍函数。Learner组件以深度神经网络作为障碍函数的模板,采用经典激活函数Re LU函数的拟合多项式作为神经网络隐藏层的合法激活函数,来构造神经网络型候选障碍函数。Verifier组件通过平方和优化方法和柱形代数分解技巧求解最差反例,并将最差反例加入Learner组件神经网络的训练集以引导下一次训练,这可以有效减少反例制导的迭代次数,最后通过柱形代数分解技巧严格保证障碍函数的正确性。实验结果表明,该方法较目前主流的障碍函数生成方法具有更好的效果和效率。·研究了基于迭代平方和规划的障碍函数生成问题。本文将深度学习和平方和规划相结合,借助平方和松弛转化障碍函数的约束条件,将障碍函数的生成问题转为平方和约束问题求解。通过给定监督学习得到的神经网络型候选障碍函数为障碍函数初值,进一步将平方和松弛造成的双线性约束求解问题转化为一组线性约束的迭代求解,从而为混成系统的安全性提供形式化保证。·实现了基于反例制导的障碍函数生成工具CEGIS4BC和基于迭代平方和规划的障碍函数生成工具SOSGS4BC,为混成系统的安全性验证提供了自动化工具。
