Exact safety verification of hybrid systems using sums-of-squares representation

Wang Lin; Min Wu; Zheng Feng Yang; Zhen Bing Zeng

doi:10.1007/s11432-013-4961-z

Exact safety verification of hybrid systems using sums-of-squares representation

Wang Lin
, Min Wu
, Zheng Feng Yang
, Zhen Bing Zeng

Software Engineering Institute

Research output: Contribution to journal › Article › peer-review

13 Scopus citations

Abstract

In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

Original language	English
Pages (from-to)	1-13
Number of pages	13
Journal	Science China Information Sciences
Volume	57
Issue number	5
DOIs	https://doi.org/10.1007/s11432-013-4961-z
State	Published - May 2014

Keywords

Symbolic computation
invariant generation
safety verification
semidefinite programming

Access to Document

10.1007/s11432-013-4961-z

Cite this

@article{345e0d087ecb421e96a523795ea19b4e,

title = "Exact safety verification of hybrid systems using sums-of-squares representation",

abstract = "In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.",

keywords = "Symbolic computation, invariant generation, safety verification, semidefinite programming",

author = "Wang Lin and Min Wu and Yang, \{Zheng Feng\} and Zeng, \{Zhen Bing\}",

year = "2014",

month = may,

doi = "10.1007/s11432-013-4961-z",

language = "英语",

volume = "57",

pages = "1--13",

journal = "Science China Information Sciences",

issn = "1674-733X",

publisher = "Science China Press ",

number = "5",

}

TY - JOUR

T1 - Exact safety verification of hybrid systems using sums-of-squares representation

AU - Lin, Wang

AU - Wu, Min

AU - Yang, Zheng Feng

AU - Zeng, Zhen Bing

PY - 2014/5

Y1 - 2014/5

N2 - In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

AB - In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares (SOS) relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

KW - Symbolic computation

KW - invariant generation

KW - safety verification

KW - semidefinite programming

UR - https://www.scopus.com/pages/publications/84899489659

U2 - 10.1007/s11432-013-4961-z

DO - 10.1007/s11432-013-4961-z

M3 - 文章

AN - SCOPUS:84899489659

SN - 1674-733X

VL - 57

SP - 1

EP - 13

JO - Science China Information Sciences

JF - Science China Information Sciences

IS - 5

ER -

Exact safety verification of hybrid systems using sums-of-squares representation

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this