微信服务号

微信订阅号

2025年4月3日 9:55 星期四
首页 > 过刊浏览>年第卷第期 >1-17. DOI:10.13328/j.cnki.jos.007176
PDF HTML阅读 XML下载 导出引用 引用提醒
基于PAC学习的组合式概率障碍证书生成
作者:
中图分类号:

TP311

基金项目:

国家重点研发计划(2022YFA1005101); 国家自然科学基金(12171159, 62272397); 上海市可信工业互联网软件协同创新中心; “数字丝绸之路”上海市可信智能软件国际联合实验室项目(22510750100)


Compositional Probabilistic Barrier Certificate Generation Based on PAC Learning
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [43]
    • | |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    连续动力系统安全验证是一个重要的研究问题, 多年来各类验证方法所能处理的问题规模非常受限. 对此, 对于给定的连续动力系统, 提出通过反例制导方法生成一组组合式概率近似正确(PAC)障碍证书的算法, 最终给出无限时间范畴安全验证问题在概率统计意义下的形式化描述. 通过建立和求解基于大M法的混合整数规划方法, 将障碍证书的求解转化为约束优化问题. 通过微分中值定理将非线性不等式进行区间线性化. 最后, 实现组合式PAC障碍证书生成工具CPBC, 并在11个基准系统上评估其性能. 实验结果表明, CPBC均能成功验证每个动力系统在指定不同的安全需求阈值下的安全性. 与现有方法相比, 所提方法可以更高效地为复杂系统或高维系统生成可靠的概率障碍证书, 验证的样例规模已高达百维.

    Abstract:

    Continuous dynamical systems safety verification is an important research issue, and over the years, various verification methods have been very limited in the scale of the problems they can handle. For a given continuous dynamical system, this study proposes an algorithm to generate a set of compositional probably approximately correct (PAC) barrier certificates through a counterexample-guided approach. A formal description of the infinite-time domain safety verification problem is given in terms of probability and statistics. By establishing and solving a mixed-integer programming method based on the Big-M method, the barrier certificate problem is transformed into a constrained optimization problem. Nonlinear inequalities are linearized in intervals using the mean value theorem of differentiation. Finally, this study implements the compositional PAC barrier certificate generator CPBC and evaluates its performance on 11 benchmark systems. The experimental results show that CPBC can successfully verify the safety of each dynamical system under specified different safety requirement thresholds. Compared with existing methods, the proposed method can more efficiently generate reliable probabilistic barrier certificates for complex or high-dimensional systems, with the verified example scale reaching up to hundreds of dimensions.

    参考文献
    [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.
    [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.
    [7] Rohn J, Kreslová J. Linear interval inequalities. Linear and Multilinear Algebra, 1994, 38(1–2): 79–82.
    [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.
    [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.
    [11] Alefeld G, Mayer G. Interval analysis: Theory and applications. Journal of Computational and Applied Mathematics, 2000, 121(1–2): 421–464.
    [12] 甘庭, 夏壁灿. 运用栅栏函数验证连续系统的有界时间安全性. 软件学报, 2016, 27(3): 645–654. http://www.jos.org.cn/1000-9825/4986.htm
    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
    [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.
    [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]
    [16] Tiwari A. Approximate reachability for linear systems. In: Proc. of the 6th Int’l Workshop on Hybrid Systems: Computation and Control. Prague: Springer, 2003. 514–525. [doi: 10.1007/3-540-36580-X_37]
    [17] Prajna S, Jadbabaie A, Pappas GJ. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. on Automatic Control, 2007, 52(8): 1415–1428.
    [18] Prajna S, Jadbabaie A. Safety verification of hybrid systems using barrier certificates. In: Proc. of the 7th Int’l Workshop on Hybrid Systems: Computation and Control. Philadelphia: Springer, 2004. 477–492. [doi: 10.1007/978-3-540-24743-2_32]
    [19] Sloth C, Pappas GJ, Wisniewski R. Compositional safety analysis using barrier certificates. In: Proc. of the 15th ACM Int’l Conf. on Hybrid Systems: Computation and Control. Beijing: ACM, 2012. 15–24. [doi: 10.1145/2185632.2185639]
    [20] Kapinski J, Deshmukh J. Discovering forward invariant sets for nonlinear dynamical systems. In: Proc. of the 2015 Interdisciplinary Topics in Applied Mathematics, Modeling and Computational Science. Cham: Springer, 2015. 259–264. [doi: 10.1007/978-3-319-12307-3_37]
    [21] Platzer A, Clarke EM. Computing differential invariants of hybrid systems as fixedpoints. In: Proc. of the 20th Int’l Conf. on Computer Aided Verification. Princeton: Springer, 2008. 176–189. [doi: 10.1007/978-3-540-70545-1_17]
    [22] Sogokon A, Ghorbal K, Tan YK, Platzer A. Vector barrier certificates and comparison systems. In: Proc. of the 22nd Int’l Symp. on Formal Methods. Oxford: Springer, 2018. 418–437. [doi: 10.1007/978-3-319-95582-7_25]
    [23] Kong H, Song XY, Han D, Gu M, Sun JG. A new barrier certificate for safety verification of hybrid systems. The Computer Journal, 2014, 57(7): 1033–1045.
    [24] Liu J, Zhan NJ, Zhao HJ. Computing semi-algebraic invariants for polynomial dynamical systems. In: Proc. of the 9th ACM Int’l Conf. on Embedded Software. Taipei: ACM, 2011. 97–106. [doi: 10.1145/2038642.2038659]
    [25] Mitchell IM, Bayen AM, Tomlin CJ. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. on Automatic Control, 2005, 50(7): 947–957.
    [26] Zeng X, Lin W, Yang ZF, Chen X, Wang LL. Darboux-type barrier certificates for safety verification of nonlinear hybrid systems. In: Proc. of the 13th Int’l Conf. on Embedded Software. Pittsburgh: ACM, 2016. 11. [doi: 10.1145/2968478.2968484]
    [27] Larsen KG, Legay A. Statistical model checking: Past, present, and future. In: Proc. of the 7th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Imperial: Springer, 2016. 3–15. [doi: 10.1007/978-3-319-47166-2_1]
    [28] Legay A, Viswanathan M. Statistical model checking: Challenges and perspectives. Int’l Journal on Software Tools for Technology Transfer, 2015, 17(4): 369–376.
    [29] Shmarov F, Zuliani P. ProbReach: Verified probabilistic delta-reachability for stochastic hybrid systems. In: Proc. of the 18th Int’l Conf. on Hybrid Systems: Computation and Control. Seattle: ACM, 2015. 134–139. [doi: 10.1145/2728606.2728625]
    [30] Shmarov F, Zuliani P. Probabilistic hybrid systems verification via SMT and Monte Carlo techniques. In: Proc. of the 12th Int’l Haifa Verification Conf. Haifa: Springer, 2016. 152–168. [doi: 10.1007/978-3-319-49052-6_10]
    [31] Ellen C, Gerwinn S, Fränzle M. Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int’l Journal on Software Tools for Technology Transfer, 2015, 17(4): 485–504.
    [32] Huang C, Chen X, Lin W, Yang ZF, Li XD. Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Trans. on Embedded Computing Systems, 2017, 16(5s): 186.
    [33] Kumar AR, Liu SL, Fisac JF, Adams RP, Ramadge PJ. ProBF: Learning probabilistic safety certificates with barrier functions. arXiv: 2112.12210, 2021.
    [34] Luo WH, Kapoor A. Airborne collision avoidance systems with probabilistic safety barrier certificates. In: Proc. of the 33rd Conf. on Neural Information Processing Systems. Vancouver: NeurIPS, 2019. 1–11.
    [35] Jing HM, Nakahira Y. Probabilistic safety certificate for multi-agent systems. In: Proc. of the 61st IEEE Conf. on Decision and Control (CDC). Cancun: IEEE, 2022. 5343–5350. [doi: 10.1109/CDC51059.2022.9992692]
    [36] 赵庆晔, 王豫, 李宣东. 安全的混成系统神经网络控制器生成与验证. 软件学报, 2023, 34(7): 2981–3001. http://www.jos.org.cn/1000-9825/6857.htm
    Zhao QY, Wang Y, Li XD. Safe neural network controller synthesis and verification for hybrid systems. Ruan Jian Xue Bao/Journal of Software, 2023, 34(7): 2981–3001 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6857.htm
    [37] Shields DN, Storey C. The behaviour of optimal Lyapunov functions. Int’l Journal of Control, 1975, 21(4): 561–573.
    [38] Ratschan S, She ZK. Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. on Embedded Computing Systems, 2007, 6(1): 8–37.
    [39] Ratschan S. Simulation based computation of certificates for safety of dynamical systems. In: Proc. of the 15th Int’l Conf. on Formal Modeling and Analysis of Timed Systems. Berlin: Springer, 2017. 303–317. [doi: 10.1007/978-3-319-65765-3_17]
    [40] Abate A, Ahmed D, Edwards A, Giacobbe M, Peruffo A. FOSSIL: A software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. In: Proc. of the 24th Int’l Conf. on Hybrid Systems: Computation and Control. Nashville: ACM, 2021. 24. [doi: 10.1145/3447928.3456646]
    [41] Llibre J, Valls C. On the integrability of the Einstein–Yang–Mills equations. Journal of Mathematical Analysis and Applications, 2007, 336(2): 1203–1230.
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

杨紫萱,曾霞,任勐鑫,王建林,曾振柄,杨争峰.基于PAC学习的组合式概率障碍证书生成.软件学报,,():1-17

复制
分享
文章指标
  • 点击次数:76
  • 下载次数: 526
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 在线发布日期: 2024-11-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19779121位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号