基于随机障碍验证的随机连续系统安全性验证

doi:10.11772/j.issn.1001-9081.2017112824

计算机应用 ›› 2018, Vol. 38 ›› Issue (6): 1737-1744.DOI: 10.11772/j.issn.1001-9081.2017112824

基于随机障碍验证的随机连续系统安全性验证

沈敏捷¹, 曾振柄², 林望³, 杨争峰¹

1. 上海市高可信计算重点实验室(华东师范大学), 上海 200062;
2. 上海大学数学系, 上海 200444;
3. 温州大学数学与信息科学学院, 浙江温州 325035

收稿日期:2017-12-01 修回日期:2018-01-31 出版日期:2018-06-10 发布日期:2018-06-13
通讯作者: 曾振柄
作者简介:沈敏捷(1993-),男,上海人,硕士研究生,主要研究方向:软件工程;曾振柄(1963-),男,甘肃皋兰人,教授,博士,主要研究方向:符号计算;林望(1982-),男,浙江温州人,副教授,博士,主要研究方向:形式化方法;杨争峰(1980-),男,安徽安庆人,副教授,博士,CCF会员,主要研究方向:软件工程。
基金资助:
国家自然科学基金资助项目（61772203，61632015，61561146394）；上海市自然科学基金资助项目（17ZR1408300）。

Safety verification of stochastic continuous system using stochastic barrier certificates

SHEN Minjie¹, ZENG Zhenbing², LIN Wang³, YANG Zhengfeng¹

1. Shanghai Key Laboratory of Trustworthy Computing(East China Normal University), Shanghai 200062, China;
2. Department of Mathematics, Shanghai University, Shanghai 200444, China;
3. College of Mathematics and Information Science, Wenzhou University, Wenzhou Zhejiang 325035, China

Received:2017-12-01 Revised:2018-01-31 Online:2018-06-10 Published:2018-06-13
Supported by:
This work is partially supported by the National Natural Science Foundation of China (61772203, 61632015, 61561146394), the Natural Science Foundation of Shanghai (17ZR1408300).

摘要/Abstract

摘要： 针对一类同时具有随机初始状态和随机微分方程的随机连续系统的安全性验证问题，提出一种基于随机障碍验证以及初始集选择的计算方法。首先，介绍了随机连续系统及其安全性验证的相关知识及概念；然后，讨论了如何对于服从几种不同分布的初始变量确定初始状态集，并根据选定的初始状态集使用随机障碍验证的方法将安全性验证问题转化为多项式优化问题；最后，运用平方和松弛方法将问题转化为平方和规划问题，并利用SOSTOOLS工具求得安全性概率的下界。理论分析以及实验结果表明，所提方法具有多项式时间的复杂度，能有效地给出随机连续系统在无界时间内的安全性概率的下界。

关键词: 连续系统, 安全性验证, 随机微分方程, 障碍验证, 平方和松弛

Abstract: Aiming at the safety verification problem of a class of stochastic continuous system equipped with both random initial state and stochastic differential equation, a new computation method based on stochastic barrier certificates and initial set selection was proposed. Firstly, the related knowledge and concepts of stochastic continuous system and its safety verification were introduced. Then, it was discussed that how to determine the initial state set for the initial variables obeying several different distributions. The safety verification problem was converted into the polynomial optimization problem by using the method of stochastic barrier certificates according to the selected initial state set. Finally, the sum of squares relaxation method was used to transform the problem into sum of squares programming problem, and the lower bound of safety probability was obtained by using the SOSTOOLS tool. The theoretical analysis and experimental results show that, the proposed method has the complexity of polynomial time and can effectively compute the lower bound of safety probability for stochastic continuous system in unbounded time.

Key words: continuous system, safety verification, stochastic differential equation, barrier certificate, sum of squares relaxation

中图分类号:

TP311.5

沈敏捷, 曾振柄, 林望, 杨争峰. 基于随机障碍验证的随机连续系统安全性验证[J]. 计算机应用, 2018, 38(6): 1737-1744.

SHEN Minjie, ZENG Zhenbing, LIN Wang, YANG Zhengfeng. Safety verification of stochastic continuous system using stochastic barrier certificates[J]. Journal of Computer Applications, 2018, 38(6): 1737-1744.

参考文献

[1] 万传军.列车自动控制系统的设计与实现[J].西安石油学院学报(自然科学版),2003,18(3):69-72.(WAN C J. Design and implementation of automatic train control system[J]. Journal of Xi'an Petroleum Institute (Natural Science Edition), 2003, 18(3):69-72.)
[2] 雷瑶.信息物理融合系统的形式化建模与分析[D].广州:广东工业大学,2013:51-65.(LEI Y. Formal Modeling and analysis of cyber physical system[D]. Guangzhou:Guangdong University of Technology, 2013:51-65.)
[3] HENZINGER T A. The theory of hybrid automata[C]//Proceedings of the the 1996 Eleventh Annual IEEE Symposium on Logic in Computer Science. Piscataway, NJ:IEEE, 1996:278-292.
[4] 卜磊,解定宝.混成系统形式化验证[J].软件学报,2014,25(2):219-233.(BU L, XIE D B. Formal verification of hybrid system[J]. Journal of Software, 2014, 25(2):219-233.)
[5] CASSANDRAS C G, LYGEROS J. Stochastic Hybrid Systems[M]. Boca Raton, Florida:Chemical Rubber Company Press, 2006:1-28.
[6] SHMAROV F, ZULIANI P. ProbReach:verified probabilistic delta-reachability for stochastic hybrid systems[C]//Proceedings of the 18th ACM International Conference on Hybrid Systems:Computation and Control. New York:ACM, 2015:134-139.
[7] BUJORIANU M L, LYGEROS J. Reachability questions in piecewise deterministic Markov processes[C]//Proceedings of the 2003 International Workshop on Hybrid Systems:Computation and Control, LNCS 2623. Berlin:Springer, 2003:126-140..
[8] HUANG C, CHEN X, LIN W, et al. Probabilistic safety verification of stochastic hybrid systems using barrier certificates[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(5s):186:1-186:19.
[9] ZHANG L J, SHE Z K, RATSCHAN S, et al. Safety verification for probabilistic hybrid systems[C]//Proceedings of the 22nd International Conference on Computer Aided Verification, LNCS 6174. Berlin:Springer, 2010:196-211.
[10] FRÄNZLE M, HAHN E M, HERMANNS H, et al. Measurability and safety verification for stochastic hybrid systems[C]//Proceedings of the 14th International Conference on Hybrid Systems:Computation and Control. New York, ACM, 2011:43-52.
[11] PRAJNA S, JADBABAIE A, PAPPAS G J. Stochastic safety verification using barrier certificates[C]//Proceedings of the 200443rd IEEE Conference on Decision and Control. Piscataway, NJ:IEEE, 2004:929-934.
[12] HU J H, LYGEROS J, SASTRY S. Towards a theory of stochastic hybrid systems[C]//Proceedings of the 2000 Third International Workshop on Hybrid Systems:Computation and Control, LNCS 1790. Berlin:Springer, 2000:160-173.
[13] BUJORIANU M L. Extended stochastic hybrid systems and their reachability problem[C]//Proceedings of the 2004 International Workshop on Hybrid Systems:Computation and Control, LNCS 2993. Berlin:Springer, 2004:234-249.
[14] DANG T, GAWLITZA T M. Discretizing affine hybrid automata with uncertainty[C]//Proceedings of the 2011 International Symposium on Automated Technology for Verification and Analysis, LNCS 6996. Berlin:Springer, 2011:473-481.
[15] KWIATKOWSKA M, NORMAN G, SPROSTON J, et al. Symbolic model checking for probabilistic timed automata[C]//Proceedings of the 2004 Joint International Conferences on Formal Techniques, Modeling and Analysis of Timed Fault-Tolerant Systmes, LNCS 3253. Berlin:Springer, 2004:293-308.
[16] ABATE A, KATOEN J P, LYGEROS J, et al. Approximate model checking of stochastic hybrid systems[J]. European Journal of Control, 2010, 16(6):624-641.
[17] ELLEN C, GERWINN S, FRÄNZLE M. Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains[J]. International Journal on Software Tools for Technology Transfer, 2015, 17(4):485-504.
[18] WANG Q S, ZULIANI P, KONG S, et al. SReach:a probabilistic bounded delta-reachability analyzer for stochastic hybrid systems[C]//Proceedings of the 2015 International Conference on Computational Methods in Systems Biology, LNCS 9308. Cham:Springer, 2015:15-27.
[19] PRAJNA S, JADBABAIE A. Safety verification of hybrid systems using barrier certificates[C]//Proceedings of the 2004 International Workshop on Hybrid Systems:Computation and Control, LNCS 2993. Berlin:Springer, 2004:477-492.
[20] PRAJNA S. Optimization-based methods for nonlinear and hybrid systems verification[D]. Pasadena, California:California Institute of Technology, 2005:39-57.
[21] MURTY K G, KABADI S N. Some NP-complete problems in quadratic and nonlinear programming[J]. Mathematical programming. 1987, 39(2):117-129.
[22] MOTZKIN T S. The arithmetic-geometric inequality[C]//Proceedings of the 1967 Symposium on Inequalities. New York:Academic Press, 1967:205-224.
[23] POWERS V, WÖRMANN T. An algorithm for sums of squares of real polynomials[J]. Journal of Pure and Applied Algebra, 1998, 127(1):99-104.
[24] PAPACHRISTODOULOU A. Scalable analysis of nonlinear systems using convex optimization[D]. Pasadena, California:California Institute of Technology, 2005:8-21.
[25] STURM J F. Using SeDuMi 1.02, a Matlab toolbox for optimization over symmetric cones[J]. Optimization Methods and Software, 1999, 11(1/2/3/4):625-653.
[26] PRAJNA S, PAPACHRISTODOULOU A, PARRILO P A. Introducing SOSTOOLS: a general purpose sum of squares programming solver [C] // Proceedings of the 41st IEEE Conference on Decision and Control. Piscataway, NJ: IEEE, 2002: 741-746.
[27] PAPACHRISTODOULOU A, PRAJNA S. A tutorial on sum of squares techniques for systems analysis [C] // Proceedings of the 2005 American Control Conference. Piscataway, NJ: IEEE, 2005: 2686-2700.
[28] EVANS L C. An Introduction to Stochastic Differential Equations [M]. Berkeley, CA: University of California-Berkeley, 2013: 79-101.
[29] BENSIMHOUN M. N-dimensional cumulative function, and other useful facts about Gaussians and normal densities [EB/OL]. [2017-10-16]. https://upload.wikimedia.org/wikipedia/commons/a/a2/Cumulative_function_n_dimensional_Gaussians_12.2013.pdf.
[30] SLOTH C, WISNIEWSKI R. Safety analysis of stochastic dynamical systems [J]. IFAC-PapersOnLine, 2015, 48(27): 62-67.

基于随机障碍验证的随机连续系统安全性验证

Safety verification of stochastic continuous system using stochastic barrier certificates

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

[1]	邹进林望罗勇曾振柄. 基于多面体包含的非线性混成系统可达性分析[J]. 计算机应用, 2013, 33(05): 1289-1293.
[2]	罗吴蔓李岩. 一种新的主动队列管理算法[J]. 计算机应用, 2008, 28(3): 596-598.
[3]	张秀山，王少明，贲可荣，徐炳良. 通用分布式仿真I/O体系结构设计及其应用[J]. 计算机应用, 2005, 25(04): 921-922.