Title
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems.
Abstract
This paper presents a linear programming (LP) relaxation based approach for generating polynomial barrier certificates for safety verification of semi-algebraic hybrid systems. The key idea is to introduce an LP relaxation to encode the set of nonnegativity constraints derived from the conditions of the associated barrier certificates and then resort to LP solvers to find the solutions. The most important benefit of the LP relaxation based approach is that it possesses a much lower computational complexity and hence can be solved very efficiently, which is demonstrated by the theoretical analysis on complexity as well as the experiment on a set of examples gathered from the literature. As far as we know, it is the first method that enables LP relaxation based polynomial barrier certificate generation.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_44
Lecture Notes in Computer Science
Keywords
Field
DocType
Formal verification,Hybrid systems,Barrier certificates,Linear programming relaxation
ENCODE,Polynomial,Computer science,Algorithm,Theoretical computer science,Linear programming,Linear programming relaxation,Hybrid system,Certificate,Formal verification,Computational complexity theory
Conference
Volume
ISSN
Citations 
9995
0302-9743
4
PageRank 
References 
Authors
0.39
23
5
Name
Order
Citations
PageRank
Zhengfeng Yang135023.43
Chao Huang272.15
Xin Chen310232.63
Wang Lin4676.82
Zhiming Liu574958.11