Barrier certificates revisited. (May 2017)

• Record Type: Journal Article
• Authors: Dai, Liyun; Gan, Ting; Xia, Bican; Zhan, Naijun
• Is Part Of: Journal of symbolic computation. Volume 80:Part 1(2017)
• Page Start: 62
• Page End: 86
• Publication Date: 2017-05
• Subjects: Hybrid system -- Barrier certificate -- Formal verification -- Invariant -- Nonlinear system -- Semi-definite programming -- Sum of squares; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2016.07.010
• Languages: English
• ISSNs: 0747-7171

Abstract

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.