KIT | KIT-Bibliothek | Impressum | Datenschutz

Deductive Stability Proofs for Ordinary Differential Equations

Tan, Yong Kiam; Platzer, André ORCID iD icon

Abstract:

Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL’s axioms with dL’s ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.


Verlagsausgabe §
DOI: 10.5445/IR/1000174210
Veröffentlicht am 16.09.2024
Originalveröffentlichung
DOI: 10.1007/978-3-030-72013-1_10
Dimensions
Zitationen: 7
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsmonat/-jahr 04.2021
Sprache Englisch
Identifikator ISBN: 978-3-030-72013-1
ISSN: 0302-9743
KITopen-ID: 1000174210
Erschienen in Tools and Algorithms for the Construction and Analysis of Systems – 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II. Ed.: J. Groote
Veranstaltung 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Stadt Luxemburg, Luxemburg, 27.03.2021 – 01.04.2021
Verlag Springer International Publishing
Seiten 181–199
Serie Lecture Notes in Computer Science (LNCS) ; 12652
Vorab online veröffentlicht am 23.03.2021
Schlagwörter differential equations, stability, differential dynamic logic
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page