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

1922 软件学报 2025 年第 36 卷第 5 期

[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. [doi: 10.1109/TAC.2007.902736]
[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. [doi: 10.1093/comjnl/bxt059]
[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. [doi: 10.1109/TAC.2005.851439]
[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. [doi: 10.1007/s10009-015-0384-z]
[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. [doi: 10.1007/s10009-014-0329-y]
[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. [doi: 10.1145/3126508]
[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] 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 [doi: 10.13328/j.cnki.
jos.006857]
[37] Shields DN, Storey C. The behaviour of optimal Lyapunov functions. Int’l Journal of Control, 1975, 21(4): 561–573. [doi: 10.1080/
00207177508922012]
[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. [doi: 10.1145/1210268.1210276]
[39] Ratschan S. Simulation based computation of certificates for safety of dynamical systems. In: Proc. of the 15th Int’l Conf. on Formal