中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 期刊论文
Title:
Barrier certificates revisited
Author: Dai, Liyun1,2; Gan, Ting1,2; Xia, Bican1,2; Zhan, Naijun3
Keyword: Hybrid system ; Barrier certificate ; Formal verification ; Invariant ; Nonlinear system ; Semi-definite programming ; Sum of squares
Source: JOURNAL OF SYMBOLIC COMPUTATION
Issued Date: 2017-05-01
DOI: 10.1016/j.jsc.2016.07.010
Volume: 80, Pages:62-86
DOC Type: Article
Indexed Type: SCI ; ISTP
WOS Headings: Science & Technology ; Technology ; Physical Sciences
WOS Subject: Computer Science, Theory & Methods ; Mathematics, Applied
WOS Subject Extended: Computer Science ; Mathematics
WOS Keyword Plus: HYBRID SYSTEMS ; ALGORITHMIC ANALYSIS ; SAFETY VERIFICATION ; INVARIANTS
English Abstract: 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.
Language: 英语
WOS ID: WOS:000390831700004
Citation statistics:
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/18862
Appears in Collections:计算机科学国家重点实验室 _期刊论文

Files in This Item:

There are no files associated with this item.


description.institution: 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

Recommended Citation:
Dai, Liyun,Gan, Ting,Xia, Bican,et al. Barrier certificates revisited[J]. JOURNAL OF SYMBOLIC COMPUTATION,2017-05-01,80:62-86.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Dai, Liyun]'s Articles
[Gan, Ting]'s Articles
[Xia, Bican]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Dai, Liyun]‘s Articles
[Gan, Ting]‘s Articles
[Xia, Bican]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace