Verifying Switched System Stability With Logic

DOI10.1145/3501710.3519541MaRDI QIDQ6120689zbMATH OpenOpenAlexWikidataFDO

Authors Yong Kiam Tan, Stefan Mitsch, André Platzer

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

differential dynamic logicloop invariantsswitched 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)

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. Moreover, the generality of the deductive approach also enables verification of switching control laws that require non-standard stability arguments through the design of loop invariants that suitably express specific intuitions behind those control laws. This flexibility is demonstrated on three case studies: a model for longitudinal flight control by Branicky, an automatic cruise controller, and Brockett's nonholonomic integrator.

Cites work

• A complete uniform substitution calculus for differential dynamic logic
• Abstraction based verification of stability of polyhedral switched systems
• Automated and sound synthesis of Lyapunov functions with SMT solvers
• Bellerophon: tactical theorem proving for hybrid systems
• Computation of piecewise quadratic Lyapunov functions for hybrid systems
• Deductive stability proofs for ordinary differential equations
• Differential equation invariance axiomatization
• Discontinuous dynamical systems
• Discovering multiple Lyapunov functions for switched hybrid systems
• dReal: an SMT solver for nonlinear theories over the reals
• Dynamical properties of hybrid automata
• scientific article; zbMATH DE number 3839814 (Why is no real title available?)
• scientific article; zbMATH DE number 1201576 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Hybrid dynamical systems
• Hybrid dynamical systems. Modeling, stability, and robustness
• Hybrid Systems: Computation and Control
• Implicit definitions with differential equations for KeYmaera X (system description)
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Logical foundations of cyber-physical systems
• Multiple Lyapunov functions and other analysis tools for switched and hybrid systems
• Nonlinear systems
• Ordinary differential equations with applications
• Simulation-guided Lyapunov analysis for hybrid dynamical systems
• Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems
• Stability analysis of switched systems with stable and unstable subsystems: an average dwell time approach
• Stability theory of switched dynamical systems
• Stabilization and tracking in the nonholonomic integrator via sliding modes
• Switching in systems and control
• Validating numerical semidefinite programming solvers for polynomial invariants
• Verifying properties of parallel programs
• Zeno hybrid systems

Cited in

(3)

• A real-analytic approach to differential-algebraic dynamic logic
• Switched systems in Coq for modeling periodic controllers
• Measuring robustness in cyber-physical systems under sensor attacks

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6120689)