research-article

Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation

Authors:

Zhengfeng Yang,

Min WuAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 14, Issue 1

Article No.: 16, Pages 1 - 19

https://doi.org/10.1145/2629424

Published: 21 January 2015 Publication History

Abstract

In this article, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via the PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which exactly satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.

References

[1]

R. Alur, T. Dang, and F. Ivancic. 2006. Predicate abstraction for reachability analysis of hybrid systems. ACM Transactions on Embedded Computing Systems 5, 1 (2006), 152--199.

Digital Library

[2]

J. Anderson and A. Papachristodoulou. 2012. A decomposition technique for nonlinear dynamical system analysis. IEEE Transactions on Automatic Control 57, 6 (2012), 1516--1521.

[3]

G. Chesi. 2010. LMI techniques for optimization over polynomials in control: a survey. IEEE Transactions on Automatic Control 55, 11 (2010), 2500--2510.

[4]

A. Chutinan and B. H. Krogh. 2003. Computational techniques for hybrid system verification. IEEE T AUTOMAT CONTR 48, 1 (2003), 64--75.

[5]

Mohab Safey El Din. 2003. RAGLib (Real Algebraic Library Maple Package). Available at http://www- calfor.lip6.fr/&sim;safey/RAGLib.

[6]

A. Dolzmann and T. Sturm. 1997. Redlog: Computer algebra meets computer logic. Acm Sigsam Bulletin 31, 2 (1997), 2--9.

Digital Library

[7]

G. H. Golub and C. F. Van Loan. 1996. Matrix Computations (3rd ed.). Johns Hopkins University Press.

Digital Library

[8]

S. Gulwani and A. Tiwari. 2008. Constraint-based approach for analysis of hybrid systems. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08). Springer, 190--203.

Digital Library

[9]

T. A. Henzinger. 1996. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 278--292.

Digital Library

[10]

E. Kaltofen, B. Li, Z. Yang, and L. Zhi. 2008. Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC’08). ACM, New York, 155--164.

Digital Library

[11]

E. Kaltofen, B. Li, Z. Yang, and L. Zhi. 2012. Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J SYMB COMPUT. 47 (2012), 1--15.

Digital Library

[12]

M. Kočvara and M. Stingl. 2003. PENNON: A code for convex nonlinear and semidefinite programming. Optimization Methods and Software 18, 3 (2003), 317--333.

[13]

M. Kočvara and M. Stingl. 2005. PENBMI User’s Guide (Version 2.0). (2005). Available at http://www.penopt.com.

[14]

G. Lafferriere, G. J. Pappas, and S. Yovine. 2001. Symbolic reachability computations for families of linear vector fields. J SYMB COMPUT. 32, 3 (2001), 231--253.

Digital Library

[15]

J. C. Lagarias. 1985. The computational complexity of simultaneous diophantine approximation problems. SIAM J COMPUT 14 (1985), 196--209.

Digital Library

[16]

J. B. Lasserre. 2010. Moments, Positive Polynomials and Their Applications. Imperial College Press.

[17]

F. Leibfritz and E. M. E. Mostafa. 2002. An interior point constrained trust region method for a special class of nonlinear semidefinite programming problems. SIAM Journal on Control and Optimization 12, 4 (2002), 1048--1074.

Digital Library

[18]

W. Lin, M. Wu, Z. Yang, and Z. Zeng. 2014. Exact safety verification of hybrid systems using sums-of-squares representation. Science China Information Sciences 57, 5 (2014), 1--13.

[19]

J. Liu, N. Zhan, and H. Zhao. 2011. Computing semi-algebraic invariants for polynomial dynamical systems. In Proceedings of the International Conference on Embedded Software (EMSOFT’11). ACM, 97--106.

Digital Library

[20]

P. Parrilo. 2003. Semidefinite programming relaxation for semialgebraic problems. Mathematical Programming Series B 96, 2 (2003), 293--320.

[21]

A. Platzer and E. M. Clarke. 2007. The image computation problem in hybrid systems model checking. In Hybrid Systems: Computation and Control, HSCC. Springer, 473--486.

Digital Library

[22]

A. Platzer and E. M. Clarke. 2009. Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in System Design 35, 1 (2009), 98--120.

Digital Library

[23]

S. Prajna. 2005. Optimization-Based Methods for Nonlinear and Hybrid Systems Verification. Ph.D. Dissertation. California Institute of Technology.

Digital Library

[24]

S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control. 477--492.

[25]

S. Ratschan and Z. She. 2006. Constraints for continuous reachability in the verification of hybrid systems. In Artificial Intelligence and Symbolic Computation. Springer, 196--210.

Digital Library

[26]

S. Ratschan and Z. She. 2007. Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Transactions of Automatic Control 6, 1 (2007), 573--589.

Digital Library

[27]

S. Ratschan and Z. She. 2010. Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM Journal on Control and Optimization 48, 7 (2010), 4377--4394.

Digital Library

[28]

E. Rodríguez-Carbonell and A. Tiwari. 2005. Generating polynomial invariants for hybrid systems. In Hybrid Systems: Computation and Control, HSCC. Lecture Notes in Computer Science, Vol. 3414. 590--605.

Digital Library

[29]

S. Sankaranarayanan, H. Sipma, and Z. Manna. 2008. Constructing invariants for hybrid systems. Formal Methods in System Design 32, 1 (2008), 25--55.

Digital Library

[30]

G. A. Shah, M. Völker, C. Sonntag, and S. Engell. 2008. A barrier certificate approach to the safety verification of a chemical reactor. In Proceedings of the 17th IFAC World Congress. 6932--6937.

[31]

C. Sloth, G. J. Pappas, and R. Wisniewski. 2012. Compositional safety analysis using barrier certificates. In Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. ACM, New York, 15--24.

Digital Library

[32]

T. Sturm and A. Tiwari. 2011. Verification and synthesis using real quantifier elimination. In Proceedings of ISSAC. ACM, New York, 329--336.

Digital Library

[33]

A. Tiwari. 2003. Approximate reachability for linear systems. In Hybrid Systems: Computation and Control, HSCC (LNCS), Vol. 2623. 514--525.

Digital Library

[34]

M. Wu and Z. Yang. 2011. Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients. In Proceedings of the 2011 International Workshop on Symbolic-Numeric Computing. ACM, New York, 104--111.

Digital Library

[35]

B. Xia. 2007. DISCOVERER: A tool for solving semi-algebraic systems. ACM Communications in Computer Algebra 41, 3 (2007), 102--103.

Digital Library

[36]

H. Yanami and H. Anai. 2007. The Maple package SyNRAC and its application to robust control design. Future Generation Computer Systems 23, 5 (2007), 721--726.

Digital Library

[37]

M. H. Zaki, S. Tahar, and G. Bois. 2007a. Combining Constraint Solving and Formal Methods for the Verification of Analog Designs. Technical Report. Concordia University.

[38]

M. H. Zaki, S. Tahar, and G. Bois. 2007b. A Symbolic approach for the safety verification of continuous systems. In Proceedings of the International Conference on Computational Sciences. 93--100.

Cited By

Zhao QChen XZhao ZZhang YTang ELi XBartocci EPutot S(2022)Verifying Neural Network Controlled Systems Using Neural NetworksProceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3501710.3519511(1-11)Online publication date: 4-May-2022
https://dl.acm.org/doi/10.1145/3501710.3519511
Xia JHu MChen XChen MOshana R(2022)Accelerated synthesis of neural network-based barrier certificates using collaborative learningProceedings of the 59th ACM/IEEE Design Automation Conference10.1145/3489517.3530608(1201-1206)Online publication date: 10-Jul-2022
https://dl.acm.org/doi/10.1145/3489517.3530608
Ding MLin KLin WDing Z(2022)A Novel Counterexample-Guided Inductive Synthesis Framework for Barrier Certificate Generation2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00034(263-273)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00034
Show More Cited By

Index Terms

Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation

Recommendations

Darboux-type barrier certificates for safety verification of nonlinear hybrid systems
EMSOFT '16: Proceedings of the 13th International Conference on Embedded Software

Benefit from less computational difficulty, barrier certificate based method has attracted much attention in safety verification of hybrid systems. Barrier certificates are inherent existences of a hybrid system and may have different types. A set of ...
Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters
HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u, x)=0, parametric ...
A hybrid integral for parametrized rational functions
SNC '07: Proceedings of the 2007 international workshop on Symbolic-numeric computation

We present a hybrid integral to obtain symbolic results of an indefinite integral where the integrand is an univariate rational function whose coeficients have a parameter. We consider calculating power series roots of the denominator polynomial by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 14, Issue 1

January 2015

443 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/2724585

Editor:
Sandeep K. Shukla
Virginia Tech, USA

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 21 January 2015

Accepted: 01 March 2014

Revised: 01 January 2014

Received: 01 April 2013

Published in TECS Volume 14, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Natural Science Foundation of China
Innovation Program of Shanghai Municipal Education Commission
Natural Science Foundation of Zhejiang Province

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
226
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)1

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhao QChen XZhao ZZhang YTang ELi XBartocci EPutot S(2022)Verifying Neural Network Controlled Systems Using Neural NetworksProceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3501710.3519511(1-11)Online publication date: 4-May-2022
https://dl.acm.org/doi/10.1145/3501710.3519511
Xia JHu MChen XChen MOshana R(2022)Accelerated synthesis of neural network-based barrier certificates using collaborative learningProceedings of the 59th ACM/IEEE Design Automation Conference10.1145/3489517.3530608(1201-1206)Online publication date: 10-Jul-2022
https://dl.acm.org/doi/10.1145/3489517.3530608
Ding MLin KLin WDing Z(2022)A Novel Counterexample-Guided Inductive Synthesis Framework for Barrier Certificate Generation2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00034(263-273)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00034
Wang QChen MXue BZhan NKatoen J(2022)Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programmingInformation and Computation10.1016/j.ic.2022.104965289(104965)Online publication date: Nov-2022
https://doi.org/10.1016/j.ic.2022.104965
Zhao QChen XZhang YSha MYang ZLin WTang EChen QLi XBogomolov SJungers R(2021)Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systemsProceedings of the 24th International Conference on Hybrid Systems: Computation and Control10.1145/3447928.3456638(1-11)Online publication date: 19-May-2021
https://dl.acm.org/doi/10.1145/3447928.3456638
Xie GYang KLuo HLi RHu S(2021)Reliability and Confidentiality Co-Verification for Parallel Applications in Distributed SystemsIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2021.304978032:6(1353-1368)Online publication date: 1-Jun-2021
https://doi.org/10.1109/TPDS.2021.3049780
Wang QChen MXue BZhan NKatoen J(2021)Synthesizing Invariant Barrier Certificates via Difference-of-Convex ProgrammingComputer Aided Verification10.1007/978-3-030-81685-8_21(443-466)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_21
Xie GLi YHan YXie YZeng GLi R(2020)Recent Advances and Future Trends for Automotive Functional Safety Design MethodologiesIEEE Transactions on Industrial Informatics10.1109/TII.2020.297888916:9(5629-5642)Online publication date: Sep-2020
https://doi.org/10.1109/TII.2020.2978889
Yang ZWu MLin W(2020)An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systemsNonlinear Analysis: Hybrid Systems10.1016/j.nahs.2019.10083736(100837)Online publication date: May-2020
https://doi.org/10.1016/j.nahs.2019.100837
Chen XPeng CLin WYang ZZhang YLi X(2020)A Novel Approach for Solving the BMI Problem in Barrier Certificates GenerationComputer Aided Verification10.1007/978-3-030-53288-8_29(582-603)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53288-8_29
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents