A linear programming relaxation based approach for generating barrier certificates of hybrid systems

Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin, Zhiming Liu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

23 Scopus citations

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.

Original languageEnglish
Title of host publicationFM 2016
Subtitle of host publicationFormal Methods - 21st International Symposium, Proceedings
EditorsConstance Heitmeyer, Anna Philippou, Stefania Gnesi, John Fitzgerald
PublisherSpringer Verlag
Pages721-738
Number of pages18
ISBN (Print)9783319489889
DOIs
StatePublished - 2016
Event21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9995 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Symposium on Formal Methods, FM 2016
Country/TerritoryCyprus
CityLimassol
Period9/11/1611/11/16

Keywords

  • Barrier certificates
  • Formal verification
  • Hybrid systems
  • Linear programming relaxation

Fingerprint

Dive into the research topics of 'A linear programming relaxation based approach for generating barrier certificates of hybrid systems'. Together they form a unique fingerprint.

Cite this