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

Safety verification of stochastic continuous system using stochastic barrier certificates

作　　者：沈敏捷 曾振柄[2] 林望[3] 杨争峰[1] SHEN Minjie 1, ZENG Zhenbing 2 , LIN Wang 3, YANG Zhengfeng 1(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)

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

出　　处：《计算机应用》2018年第6期1737-1744,1750,共9页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61772203;61632015;61561146394);上海市自然科学基金资助项目(17ZR1408300)~~

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]