publication . Preprint . Article . Other literature type . 2018

Converse Theorems for Safety and Barrier Certificates

Ratschan, Stefan;
Open Access English
  • Published: 01 Aug 2018
  • Country: Czech Republic
An important tool for proving safety of dynamical systems is the notion of a barrier certificate. In this technical note we prove that every robustly safe ordinary differential equation has a barrier certificate. Moreover, we show a construction of such a barrier certificate based on a set of states that is reachable in finite time.
arXiv: Computer Science::Cryptography and SecurityComputer Science::Symbolic Computation
ACM Computing Classification System: ComputingMilieux_THECOMPUTINGPROFESSION
free text keywords: Safety, Robustness, Radio frequency, Differential equations, Tools, Computer science, Computer Science - Systems and Control, Control and Systems Engineering, Electrical and Electronic Engineering, Computer Science Applications, Controllability, Differential equation, Applied mathematics, Dynamical systems theory, Mathematics, Certificate, Mathematical optimization, Converse, Robustness (computer science), Ordinary differential equation, Finite time
Related Organizations
17 references, page 1 of 2

[1] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unied lattice model for static analysis of programs by construction or approximation of xpoints. In Fourth ACM Symposium on Principles of Programming Languages, pages 238{252, 1977.

[2] Werner Damm, Guilherme Pinto, and Stefan Ratschan. Guaranteed termination in the veri cation of LTL properties of non-linear robust discrete time hybrid systems. International Journal of Foundations of Computer Science (IJFCS), 18(1):63{86, 2007.

[3] Martin Franzle. Analysis of hybrid systems: An ounce of realism can save an in nity of states. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (CSL'99), number 1683 in LNCS. Springer, 1999.

[4] Goran Frehse. Phaver: algorithmic veri cation of hybrid systems past HyTech. International Journal on Software Tools for Technology Transfer (STTT), 10(3):263{279, 2008.

[5] Khalil Ghorbal, Andrew Sogokon, and Andre Platzer. A hierarchy of proof rules for checking positive invariance of algebraic and semialgebraic sets. Computer Languages, Systems & Structures, 2016.

[6] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HYTECH: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer (STTT), 1:110{122, 1997.

[7] Morris W. Hirsch, Stephen Smale, and Robert L. Devaney. Di erential Equations, Dynamical Systems, and an Introduction to Chaos. Academic Press, 2nd edition edition, 2003.

[8] J. H. Hubbard and B. B. Hubbard. Vector Calculus, Linear Algebra, And Di erential Forms. Matrix Editions, 2001.

[9] Hassan K. Khalil. Nonlinear Systems. Prentice Hall, 3rd edition, 2002.

[10] Henk Nijmeijer and Arjan Van der Schaft. Nonlinear dynamical control systems. Springer-Verlag New York, 1990.

[11] Stephen Prajna and Ali Jadbabaie. Safety veri cation of hybrid systems using barrier certi cates. In Rajeev Alur and George J. Pappas, editors, HSCC'04, number 2993 in LNCS. Springer, 2004.

[12] Stephen Prajna and Anders Rantzer. On the necessity of barrier certi cates. In Proceedings of the IFAC World Congress, Prague, Czech Republic, July 2005.

[13] Stephen Prajna and Anders Rantzer. Convex programs for temporal veri cation of nonlinear dynamical systems. SIAM Journal on Control and Optimization, 46(3):999{1021, 2007.

[14] Stefan Ratschan. Safety veri cation of non-linear hybrid systems is quasi-decidable. Formal Methods in System Design, 44(1):71{90, 2014.

[15] Shankar Sastry. Nonlinear systems: analysis, stability, and control. Springer-Verlag New York, 1999.

17 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Preprint . Article . Other literature type . 2018

Converse Theorems for Safety and Barrier Certificates

Ratschan, Stefan;