Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients

Min Wu; Zhengfeng Yang

doi:10.1145/2331684.2331701

Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients

Min Wu^*
, Zhengfeng Yang

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

6 Scopus citations

Abstract

In this paper we discuss how to generate inequality invariants for continuous dynamical systems involved in hybrid systems. A hybrid symbolic-numeric algorithm is presented to compute inequality invariants of the given systems, by transforming this problem into a parameterized polynomial optimization problem. A numerical inequality invariant of the given system can be obtained by applying polynomial Sum-of-Squares (SOS) relaxation via Semidefinite Programming (SDP). And a method based on Gauss-Newton refinement is deployed to obtain candidates of polynomials with rational coefficients, and finally we certify that this polynomial exactly satisfies the conditions of invariants, by use of SOS representation of polynomials with rational coefficients. Several examples are given to show that our algorithm can successfully yield inequality invariants with rational coefficients.

Original language	English
Title of host publication	SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation
Pages	104-111
Number of pages	8
DOIs	https://doi.org/10.1145/2331684.2331701
State	Published - 2011
Event	SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation - San Jose, CA, United States Duration: 7 Jun 2011 → 9 Jun 2011

Publication series

Name	SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation

Conference

Conference	SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation
Country/Territory	United States
City	San Jose, CA
Period	7/06/11 → 9/06/11

Keywords

Differential invariant
Program verification
Semidefinite programming
Sum-of-squares relaxation

Access to Document

10.1145/2331684.2331701

Cite this

@inproceedings{463479c7630345c0898828e980c6530f,

title = "Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients",

abstract = "In this paper we discuss how to generate inequality invariants for continuous dynamical systems involved in hybrid systems. A hybrid symbolic-numeric algorithm is presented to compute inequality invariants of the given systems, by transforming this problem into a parameterized polynomial optimization problem. A numerical inequality invariant of the given system can be obtained by applying polynomial Sum-of-Squares (SOS) relaxation via Semidefinite Programming (SDP). And a method based on Gauss-Newton refinement is deployed to obtain candidates of polynomials with rational coefficients, and finally we certify that this polynomial exactly satisfies the conditions of invariants, by use of SOS representation of polynomials with rational coefficients. Several examples are given to show that our algorithm can successfully yield inequality invariants with rational coefficients.",

keywords = "Differential invariant, Program verification, Semidefinite programming, Sum-of-squares relaxation",

author = "Min Wu and Zhengfeng Yang",

year = "2011",

doi = "10.1145/2331684.2331701",

language = "英语",

isbn = "9781450305150",

series = "SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation",

pages = "104--111",

booktitle = "SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation",

note = "SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation ; Conference date: 07-06-2011 Through 09-06-2011",

}

Wu, M & Yang, Z 2011, Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients. in SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation. SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation, pp. 104-111, SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation, San Jose, CA, United States, 7/06/11. https://doi.org/10.1145/2331684.2331701

Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients. / Wu, Min; Yang, Zhengfeng.
SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation. 2011. p. 104-111 (SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients

AU - Wu, Min

AU - Yang, Zhengfeng

PY - 2011

Y1 - 2011

N2 - In this paper we discuss how to generate inequality invariants for continuous dynamical systems involved in hybrid systems. A hybrid symbolic-numeric algorithm is presented to compute inequality invariants of the given systems, by transforming this problem into a parameterized polynomial optimization problem. A numerical inequality invariant of the given system can be obtained by applying polynomial Sum-of-Squares (SOS) relaxation via Semidefinite Programming (SDP). And a method based on Gauss-Newton refinement is deployed to obtain candidates of polynomials with rational coefficients, and finally we certify that this polynomial exactly satisfies the conditions of invariants, by use of SOS representation of polynomials with rational coefficients. Several examples are given to show that our algorithm can successfully yield inequality invariants with rational coefficients.

AB - In this paper we discuss how to generate inequality invariants for continuous dynamical systems involved in hybrid systems. A hybrid symbolic-numeric algorithm is presented to compute inequality invariants of the given systems, by transforming this problem into a parameterized polynomial optimization problem. A numerical inequality invariant of the given system can be obtained by applying polynomial Sum-of-Squares (SOS) relaxation via Semidefinite Programming (SDP). And a method based on Gauss-Newton refinement is deployed to obtain candidates of polynomials with rational coefficients, and finally we certify that this polynomial exactly satisfies the conditions of invariants, by use of SOS representation of polynomials with rational coefficients. Several examples are given to show that our algorithm can successfully yield inequality invariants with rational coefficients.

KW - Differential invariant

KW - Program verification

KW - Semidefinite programming

KW - Sum-of-squares relaxation

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

U2 - 10.1145/2331684.2331701

DO - 10.1145/2331684.2331701

M3 - 会议稿件

AN - SCOPUS:84865021197

SN - 9781450305150

T3 - SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation

SP - 104

EP - 111

BT - SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation

T2 - SNC'11 - Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation

Y2 - 7 June 2011 through 9 June 2011

ER -

Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this