Barrier certificates revisited

doi:10.1016/j.jsc.2016.07.010

	Barrier certificates revisited
	Dai, Liyun1,2; Gan, Ting1,2; Xia, Bican1,2; Zhan, Naijun3
	2017-05-01
发表期刊	JOURNAL OF SYMBOLIC COMPUTATION
卷号	80 页码:62-86
摘要	A barrier certificate can separate the state space of a considered hybrid system (HS) into safe and unsafe parts according to the safety property to be verified. Therefore this notion has been widely used in the verification of HSs. A stronger condition on barrier certificates (BCs) means that fewer BCs can be synthesized, as the expressiveness of synthesized BCs is weaker. On the other hand, synthesizing more expressive BCs normally means higher complexity. Kong et al. (2013a) investigated how to relax the condition of BCs while still keeping their convexity so that one can synthesize more expressive BCs efficiently using semi-definite programming (SDP). In this paper, we first discuss how to relax the condition of BCs in a general way, while still keeping their convexity. Thus, one can utilize different weaker conditions flexibly to synthesize different kinds of BCs with more expressiveness efficiently using SDP, which gives more opportunities to verify the considered system. We also show how to combine two functions together to form a combined BC in order to prove a safety property under consideration, whereas neither of them may be a BC separately. In fact, the notion of combined BCs is strictly more expressive than that of BCs, so it further brings more chances to verify a considered system. Another contribution of this paper is to investigate how to avoid the unsoundness of SDP based approaches caused by numerical error through symbolic checking. (C) 2016 Elsevier Ltd. All rights reserved.
收录类别	SCI ; ISTP
文章类型	Article
关键词	Hybrid System Barrier Certificate Formal Verification Invariant Nonlinear System Semi-definite Programming Sum Of Squares
WOS标题词	Science & Technology ; Technology ; Physical Sciences
类目[WOS]	Computer Science, Theory & Methods ; Mathematics, Applied
DOI	10.1016/j.jsc.2016.07.010
研究领域[WOS]	Computer Science ; Mathematics
关键词[WOS]	HYBRID SYSTEMS ; ALGORITHMIC ANALYSIS ; SAFETY VERIFICATION ; INVARIANTS
语种	英语
WOS记录号	WOS:000390831700004
引用统计
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/18862
专题	基础软件与系统重点实验室
作者单位	1.Peking Univ, LMAM, Beijing, Peoples R China 2.Peking Univ, Sch Math Sci, Beijing, Peoples R China 3.Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100864, Peoples R China
推荐引用方式 GB/T 7714	Dai, Liyun,Gan, Ting,Xia, Bican,et al. Barrier certificates revisited[J]. JOURNAL OF SYMBOLIC COMPUTATION,2017,80:62-86.
APA	Dai, Liyun,Gan, Ting,Xia, Bican,&Zhan, Naijun.(2017).Barrier certificates revisited.JOURNAL OF SYMBOLIC COMPUTATION,80,62-86.
MLA	Dai, Liyun,et al."Barrier certificates revisited".JOURNAL OF SYMBOLIC COMPUTATION 80(2017):62-86.