Converse Theorems for Safety and Barrier Certificates

Preprint English OPEN
Ratschan, Stefan (2017)
  • Subject: Computer Science - Systems and Control
    arxiv: Computer Science::Symbolic Computation | Computer Science::Cryptography and Security
    acm: ComputingMilieux_THECOMPUTINGPROFESSION

An important tool for proving safety of dynamical systems is the notion of a barrier certificate. In this paper 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.
  • References (17)
    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.

  • Metrics
    No metrics available
Share - Bookmark