An official website of the United States government
This paper addresses the problem of hybrid control for a class of switched uncertain systems. The switched system under consideration is subject to structured uncertain dynamics in a linear fractional transformation (LFT) form and time-varying input delays. A novel hybrid controller is proposed, which consists of three major components: the integral quadratic constraint (IQC) dynamics, the continuous dynamics, and the jump dynamics. The IQC dynamics are developed by leveraging methodologies from robust control theory and are utilised to address the effects of time-varying input delays. The continuous dynamics are structured by feeding back not only measurement outputs but also some system's internal signals. The jump dynamics enforce a jump (update/reset) at every switching time instant for the states of both IQC dynamics and continuous dynamics. Based on this, robust stability of the overall hybrid closed-loop system is established under the average dwell time framework with multiple Lyapunov functions. Moreover, the associated control synthesis conditions are fully characterised as linear matrix inequalities, which can be solved efficiently. An application example on regulation of a nonlinear switched electronic circuit system has been used to demonstrate effectiveness and usefulness of the proposed approach.
more »
« less
Verifying Switched System Stability With Logic
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.
more »
« less
- Award ID(s):
- 1739629
- PAR ID:
- 10359323
- Editor(s):
- Bartocci, Ezio; Putot, Sylvie
- Date Published:
- Journal Name:
- Hybrid Systems: Computation and Control (part of CPS Week 2022), HSCC'22
- Page Range / eLocation ID:
- 1 to 11
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Program verification offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind automated verification of real-world programs which often contain many loops. In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces. We develop a new sound and complete semantic mapping for assigning SMT formulas to continuous truth values that allows CLNs to be trained efficiently. We use CLNs to implement a new inference system for loop invariants, CLN2INV, that significantly outperforms existing approaches on the popular Code2Inv dataset. CLN2INV is the first tool to solve all 124 theoretically solvable problems in the Code2Inv dataset. Moreover, CLN2INV takes only 1.1 seconds on average for each problem, which is 40× faster than existing approaches. We further demonstrate that CLN2INV can even learn 12 significantly more complex loop invariants than the ones required for the Code2Inv dataset.more » « less
-
Functional electrical stimulation (FES) induced cycling provides a means of therapeutic exercise and functional restoration for people affected by neuromuscular disorders. A challenge in closed-loop FES control of coordinated motion is the presence of a potentially destabilizing input delay between the application of the electrical stimulation and the resulting muscle contraction. Moreover, switching amongst multiple actuators (e.g., between FES control of various muscle groups and a controlled electric motor) presents additional challenges for overall system stability. In this paper, a closed-loop controller is developed to yield exponential cadence tracking, despite an unknown input delay, switching between FES and motor only control, uncertain nonlinear dynamics, and additive disturbances. Lyapunov-Krasovskii functionals are used in a Lyapunov-based stability analysis to ensure exponential convergence for all time.more » « less
-
Continuous invariants are an important ingredient for deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges for automating formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.more » « less
-
null (Ed.)Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus : an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3501710.3519541
