Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Ratschan, Stefan (2017)
Languages: English
Types: Preprint
Subjects: Computer Science - Systems and Control

Classified by OpenAIRE into

arxiv: Computer Science::Cryptography and Security, Computer Science::Symbolic Computation
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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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.
    • [16] Ankur Taly and Ashish Tiwari. Deductive veri cation of continuous dynamical systems. In Ravi Kannan and K Narayan Kumar, editors, IARCS Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009), volume 4 of Leibniz International Proceedings in Informatics (LIPIcs), pages 383{394, Dagstuhl, Germany, 2009.
    • [17] R. Wisniewski and C. Sloth. Converse barrier certi cate theorems. IEEE Transactions on Automatic Control, 61(5):1356{1361, 2016.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article

Collected from