Source-linked AI summary
Approximately bisimilar symbolic models for incrementally stable switched systems
Antoine Girard, Giordano Pola, Paulo Tabuada
TL;DR
Switched systems need abstractions supporting objectives beyond stability analysis. This paper constructs approximately bisimilar symbolic models under incremental-stability assumptions and uses them for controller synthesis. The resulting abstractions can be finite, effectively computable, and arbitrarily precise, with two controller-design examples.
Problem
Existing progress on switched-system stability and stabilization does not address the paper's broader need for symbolic abstractions supporting more complex objectives.
Method
The paper constructs symbolic models using approximate bisimulation under a common Lyapunov function or multiple Lyapunov functions with dwell time, with sampled switching dynamics represented explicitly.
Results
Under incremental-stability assumptions, approximately bisimilar symbolic models exist with any chosen precision, and the paper demonstrates controller design on two switched-system examples.
Takeaways & Limitations
The abstractions are constructively and effectively computable, can be finite for bounded state spaces, and support algorithmic controller synthesis.
Takeaways & Limitations
The resulting controllers may have complex switching surfaces, increasing controller space complexity and complicating real-time implementation; dwell-time enforcement can also enlarge symbolic models.
Abstract
from arXiv · showhide
Switched systems constitute an important modeling paradigm faithfully describing many engineering systems in which software interacts with the physical world. Despite considerable progress on stability and stabilization of switched systems, the constant evolution of technology demands that we make similar progress with respect to different, and perhaps more complex, objectives. This paper describes one particular approach to address these different objectives based on the construction of approximately equivalent (bisimilar) symbolic models for switched systems. The main contribution of this paper consists in showing that under standard assumptions ensuring incremental stability of a switched system (i.e. existence of a common Lyapunov function, or multiple Lyapunov functions with dwell time), it is possible to construct a finite symbolic model that is approximately bisimilar to the original switched system with a precision that can be chosen a priori. To support the computational merits of the proposed approach, we use symbolic models to synthesize controllers for two examples of switched systems, including the boost DC-DC converter.
1. Introduction
The paper motivates symbolic abstractions for switched systems, linking approximately bisimilar models to controller synthesis for more complex objectives.
- Switched systems model engineering systems in which software interacts with the physical world.
- Switching among stable subsystems can nevertheless render the overall system unstable, motivating analysis of stabilizing switching strategies.
- Symbolic models abstract switched dynamics by mapping each abstract symbol to an aggregate of original-system states.
- Finite symbolic models enable efficient controller synthesis using supervisory-control and algorithmic-game-theory techniques.
- Approximate bisimulation relaxes exact output equality to closeness, enabling symbolic models for larger classes of incrementally stable systems.
2. Switched systems and incremental stability
The paper formalizes switched systems and extends incremental stability analysis to switching signals, using common or multiple Lyapunov functions to establish uniform convergence.
- Switched systems: A switched system comprises a continuous state space, finitely many modes, admissible piecewise-constant switching signals, and mode-indexed locally Lipschitz vector fields.
- Switched systems: Each mode defines a continuous subsystem governed by its vector field, with solutions assumed to exist on an interval extending beyond the initial time.
- Switched systems: Switching signals have finitely many discontinuities on bounded intervals, ensuring trajectory existence and uniqueness while ruling out Zeno behavior.
- Incremental stability: δ-GUAS requires trajectories under every common switching signal to converge uniformly according to a class-KL bound.
- Incremental stability: A common δ-GAS Lyapunov function implies δ-GUAS for the switched system, with convergence bound β(r,s)=α^-1(α(r)e^-κs).
- Incremental stability: When no common Lyapunov function exists, multiple δ-GAS Lyapunov functions combined with dwell-time switching can ensure δ-GUAS.
3. Approximate bisimulation
The paper represents switched systems as metric transition systems and defines approximate bisimulation as mutual transition matching with outputs allowed to differ within a chosen precision.
- A transition system contains states, labels, transitions, outputs, an output function, and initial states.
- Metric transition systems equip the output set with a metric, while finite systems have finite state and label sets.
- The transition relation records how a system evolves from one state to another under a labeled action.
- A switched system becomes a transition system whose states are continuous states, labels pair modes with durations, and outputs are the states themselves.
- Approximate bisimulation replaces equality of observed behaviors with output closeness while requiring matching transitions in both directions.
4. Approximately bisimilar symbolic models
The paper constructs sampled symbolic models on lattices and proves their approximate bisimilarity to switched systems under incremental-stability assumptions. A common Lyapunov function supports arbitrary sampling rates, while multiple Lyapunov functions require dwell time; compact-state restrictions make the models finite for computation.
- Sampled transition systems: Sampling restricts switching instants to multiples of τs and represents the switched system as a transition system with state, label, output, and initial-state structures.The sampled model uses duration-τs trajectories; with dwell time, the state additionally records the active subsystem and elapsed time since switching.
- Lattice abstraction: The symbolic abstraction replaces R^n with a lattice [R^n]_η, whose points approximate every continuous state within distance η.The resulting symbolic transition system is countable, uses the same labels and outputs, and observes each lattice point through the natural inclusion map.
- Common Lyapunov function: Under a common δ-GAS Lyapunov function, a constructive relation based on Lyapunov sublevel sets proves ε-approximate bisimilarity between the sampled system and its symbolic model.The relation bounds state-output discrepancies by ε and is preserved through sampled transitions using Lyapunov contraction and lattice approximation.
- Common Lyapunov function: For a common δ-GAS Lyapunov function, sufficiently small η achieves any desired precision ε for every sampling rate τs.Using Lyapunov sublevel sets, rather than an infinity-norm relation, also permits arbitrarily small sampling parameters and supports extension to multiple Lyapunov functions.
- Multiple Lyapunov functions: When no common δ-GAS Lyapunov function exists, approximate bisimilarity remains available under a dwell-time restriction represented by elapsed-switching-time state variables.The required dwell-time lower bound matches the bound ensuring incremental stability; sufficiently large dwell time permits arbitrary precision.
- Practical computation: Restricting the symbolic state space to a compact subset produces finite models, with transition computation based mainly on numerical simulation and errors incorporated by replacing η with η + e.On compact subsets, the Lyapunov regularity condition requires no assumptions beyond the common or multiple Lyapunov functions ensuring incremental stability.
5. Examples of symbolic control design
Two examples show how approximately bisimilar symbolic models support controller synthesis for switched systems, including a boost DC-DC converter and a two-mode system with multiple Lyapunov functions.
- The examples illustrate the effectiveness of the paper’s symbolic-model approach for switched-system control design.
- 5.1. Common Lyapunov functions: the boost DC-DC converter.: For the boost DC-DC converter, the control goal is to keep the inductor current near a reference by maintaining the state in an invariant set.
- 5.1. Common Lyapunov functions: the boost DC-DC converter.: The converter’s two subsystems are incrementally stable and share a common δ-GAS Lyapunov function, although the switched system is not GAS because their equilibria differ.
- 5.1. Common Lyapunov functions: the boost DC-DC converter.: For the converter, achieving precision ε requires a discretization parameter satisfying η ≤ ε/145; weak subsystem stability makes the approximation ratio large.
- 5.1. Common Lyapunov functions: the boost DC-DC converter.: With ε = 0.026, the converter model has 642001 states, while model construction and supervisory-controller synthesis take less than 60 seconds.
- 5.2. Multiple Lyapunov functions.: The second two-mode example uses a safety specification that keeps trajectories in I while avoiding unsafe states U containing both equilibria.
- 5.2. Multiple Lyapunov functions.: Its symbolic model contains 7696008 states, yet construction and controller synthesis take about 130 seconds for precision ε = 0.34.
- 5.2. Multiple Lyapunov functions.: The synthesized controller distinguishes mandatory mode choices, states allowing either mode, and uncontrollable states when switching is enabled.
6. Conclusion
Under incremental-stability assumptions, the paper constructs effectively computable approximately bisimilar symbolic abstractions for switched systems with arbitrary precision, and demonstrates controller design through two examples. The authors identify controller complexity and dwell-time enforcement as directions for improvement.
- Common or multiple δ-GAS Lyapunov functions with dwell time ensure the existence of approximately bisimilar symbolic abstractions for switched systems.
- The constructive proof makes the abstractions effectively computable and allows any desired precision.
- Two non-trivial examples demonstrate controller design based on symbolic models of switched systems.
- Controllers for arbitrary specifications may require complex switching surfaces, increasing space complexity and complicating real-time implementation.
- The authors are investigating conservative lower-complexity controllers and enforcing dwell time through specifications to obtain smaller symbolic models.