Verifying Switched System Stability With Logic

DOI10.1145/3501710.3519541arXiv2111.01928OpenAlexW3211178120MaRDI QIDQ6120689

Stefan Mitsch, André Platzer, Yong Kiam Tan

Publication date: 21 February 2024

Published in: 25th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2111.01928

zbMATH Keywords

loop invariantsdifferential dynamic logicswitched system stability

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stability theory of switched dynamical systems
• Stabilization and tracking in the nonholonomic integrator via sliding modes
• Switching in systems and control
• Bellerophon: tactical theorem proving for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• Implicit definitions with differential equations for KeYmaera X (system description)
• Abstraction based verification of stability of polyhedral switched systems
• Deductive stability proofs for ordinary differential equations
• Zeno hybrid systems
• Stabhyli
• Simulation-guided lyapunov analysis for hybrid dynamical systems
• Stability analysis of switched systems with stable and unstable subsystems: an average dwell time approach
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Verifying properties of parallel programs
• Multiple Lyapunov functions and other analysis tools for switched and hybrid systems
• Computation of piecewise quadratic Lyapunov functions for hybrid systems
• Logical Foundations of Cyber-Physical Systems
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Logical Analysis of Hybrid Systems
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
• Differential Equation Invariance Axiomatization
• Discovering Multiple Lyapunov Functions for Switched Hybrid Systems
• Dynamical properties of hybrid automata
• Discontinuous dynamical systems
• Hybrid dynamical systems
• Hybrid Systems: Computation and Control
• Validating numerical semidefinite programming solvers for polynomial invariants

This page was built for publication: Verifying Switched System Stability With Logic