We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

eess.SY

Change to browse by:

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Electrical Engineering and Systems Science > Systems and Control

Title: Verifying Switched System Stability With Logic

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.
Comments: Long version of paper at HSCC 2022 (25th ACM International Conference on Hybrid Systems: Computation and Control, May 4-6, 2022)
Subjects: Systems and Control (eess.SY); Logic in Computer Science (cs.LO)
MSC classes: 03B70, 34A38, 93C30
ACM classes: F.3.1; F.4.1; G.1.7; I.2.3
DOI: 10.1145/3501710.3519541
Cite as: arXiv:2111.01928 [eess.SY]
  (or arXiv:2111.01928v2 [eess.SY] for this version)

Submission history

From: Yong Kiam Tan [view email]
[v1] Tue, 2 Nov 2021 22:40:29 GMT (427kb,D)
[v2] Fri, 8 Apr 2022 19:09:53 GMT (393kb,D)

Link back to: arXiv, form interface, contact.