KIT | KIT-Bibliothek | Impressum | Datenschutz

Verifying Switched System Stability With Logic

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

Abstract:

Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closed-loop systems that arise from their proposed switching control laws. This paper presents a formal approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL), a logic for deductive verification of hybrid systems. From controls, we use standard stability notions for various classes of switching mechanisms and their corresponding Lyapunov function-based analysis techniques. From verification, we use dL’s ability to verify quantified properties of hybrid systems and dL models of switched systems as looping hybrid programs whose stability can be formally specified and proven by finding appropriate loop invariants, i.e., properties that are preserved across each loop iteration. This blend of ideas enables a trustworthy implementation of switched system stability verification in the KeYmaera X prover based on dL. For standard classes of switching mechanisms, the implementation provides fully automated stability proofs, including searching for suitable Lyapunov functions. ... mehr


Verlagsausgabe §
DOI: 10.5445/IR/1000174208
Veröffentlicht am 16.09.2024
Originalveröffentlichung
DOI: 10.1145/3501710.3519541
Scopus
Zitationen: 5
Dimensions
Zitationen: 3
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 04.05.2022
Sprache Englisch
Identifikator ISBN: 978-1-4503-9196-2
KITopen-ID: 1000174208
Erschienen in HSCC '22: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control
Veranstaltung 25th ACM International Conference on Hybrid Systems: Computation and Control (2022), Mailand, Italien, 04.05.2022 – 06.05.2022
Verlag Association for Computing Machinery (ACM)
Seiten 1–11
Schlagwörter switched system stability, loop invariants, differential dynamic logic
Nachgewiesen in Scopus
Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page