Page 21 - 《软件学报》2025年第5期

杨紫萱 等: 基于 PAC 学习的组合式概率障碍证书生成 1921

7 总 结

本文提出基于反例制导方法学习一组组合式 PAC 障碍证书的算法, 以解决非线性连续动力系统概率安全验
证中的不确定性和高维状态空间等挑战. 将求解 PAC 障碍证书的优化问题转化为基于大 M 法的混合整数规划问
题. 对于在 3 个区域上的不等式约束, 通过使用场景优化方法和基于微分中值定理的区间线性化方法, 将其转化为
线性优化问题, 并通过数值优化器 Gurobi 进行求解. 最后对 11 个非线性连续动力系统进行对比实验. 实验结果表
明, 本文提出的 CPBC 算法在不需要对区域进行划分的情况下, 成功验证了所有用例的概率安全性, 同时证明了基
于微分中值定理的区间线性化方法能更接近原始非线性约束, 从而得到最优解. 综合实验结果, 本文为实际系统的
安全性评估提供了实用且可靠的方法, 有望推动非线性连续动力系统概率安全性验证领域的发展.
在区间线性化过程中, 可以将区间分割成多个部分, 并使用中值定理来提高精度, 从而有望减少组合式障碍证
书的数量, 但会显著增加求解时间. 本文所提方法不使用区域划分, 而是通过构造组合式障碍证书来平衡精度问题
和前期计算的要求. 未来, 我们将探索如何平衡区域划分带来的 PAC 障碍证书数量与求解时间, 以进一步提高算
法的效率和实用性.

References:
[1] Chen B, Li TF. Formal modeling and verification of autonomous driving scenario. In: Proc. of the 2021 IEEE Int’l Conf. on Information
Communication and Software Engineering (ICICSE). Chengdu: IEEE, 2021. 313–321. [doi: 10.1109/ICICSE52190.2021.9404128]
[2] Jiang Y, Song HB, Wang R, Gu M, Sun JG, Sha L. Data-centered runtime verification of wireless medical cyber-physical system. IEEE
Trans. on Industrial Informatics, 2017, 13(4): 1900–1909. [doi: 10.1109/TII.2016.2573762]
[3] Wang Q, Turriate V, Burgos R, Boroyevich D, Sagona J, Kheraluwala M. Towards a high performance motor drive for aerospace
applications: Topology evaluation, converter optimization and hardware verification. In: Proc. of the 43rd Annual Conf. of the IEEE
Industrial Electronics Society (IECON 2017). Beijing: IEEE, 2017. 1622–1628. [doi: 10.1109/IECON.2017.8216275]
[4] Haussler D. Probably approximately correct learning. In: Proc. of the 8th National Conf. on Artificial Intelligence. Boston: ACM, 1990.
1101–1108. [doi: 10.5555/1865609.1865663]
[5] Xue B, Fränzle M, Zhao HJ, Zhan NJ, Easwaran A. Probably approximate safety verification of hybrid dynamical systems. In: Proc. of
the 21st Int’l Conf. on Formal Engineering Methods. Shenzhen: Springer, 2019. 236–252. [doi: 10.1007/978-3-030-32409-4_15]
[6] Campi MC, Garatti S, Prandini M. The scenario approach for systems and control design. Annual Reviews in Control, 2009, 33(2):
149–157. [doi: 10.1016/j.arcontrol.2009.07.001]
[7] Rohn J, Kreslová J. Linear interval inequalities. Linear and Multilinear Algebra, 1994, 38(1–2): 79–82. [doi: 10.1080/030810895088
18341]
[8] Hladík M. Interval linear programming: A survey. In: Mann ZA, ed. Linear Programming—New Frontiers in Theory and Applications.
New York: Nova Science Publishers, 2012. 85–120.
[9] Hladík M. Optimal value range in interval linear programming. Fuzzy Optimization and Decision Making, 2009, 8(3): 283–294. [doi: 10.
1007/s10700-009-9060-7]
[10] Hladík M. Weak and strong solvability of interval linear systems of equations and inequalities. Linear Algebra and its Applications, 2013,
438(11): 4156–4165. [doi: 10.1016/j.laa.2013.02.012]
[11] Alefeld G, Mayer G. Interval analysis: Theory and applications. Journal of Computational and Applied Mathematics, 2000, 121(1–2):
421–464. [doi: 10.1016/S0377-0427(00)00342-3]
[12] Gan T, Xia BC. Barrier certificate generation for safety verification of continuous systems for a bounded time. Ruan Jian Xue Bao/
Journal of Software, 2016, 27(3): 645–654 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4986.htm [doi: 10.13328/
j.cnki.jos.004986]
[13] Gulwani S, Tiwari A. Constraint-based approach for analysis of hybrid systems. In: Proc. of the 20th Int’l Conf. on Computer Aided
Verification. Princeton: Springer, 2008. 190–203. [doi: 10.1007/978-3-540-70545-1_18]
[14] Kapinski J, Deshmukh JV, Sankaranarayanan S, Aréchiga N. Simulation-guided Lyapunov analysis for hybrid dynamical systems. In:
Proc. of the 17th Int’l Conf. on Hybrid Systems: Computation and Control. Berlin: ACM, 2014. 133–142. [doi: 10.1145/2562059.
2562139]
[15] Sankaranarayanan S, Sipma HB, Manna Z. Constructing invariants for hybrid systems. In: Proc. of the 7th Int’l Workshop on Hybrid
Systems: Computation and Control. Philadelphia: Springer, 2004. 539–554. [doi: 10.1007/978-3-540-24743-2_36]