Source-linked AI summary
Symbolic Models for Nonlinear Control Systems: Alternating Approximate Bisimulations
Giordano Pola, Paulo Tabuada
TL;DR
The paper addresses symbolic modeling for nonlinear control systems affected by disturbances, where standard approximate bisimulation does not distinguish control and disturbance inputs. It introduces alternating approximate bisimulation and shows that incrementally globally asymptotically stable nonlinear systems admit symbolic models, with easily computable constructions for asymptotically stable linear systems.
Problem
Symbolic models can reduce controller-synthesis complexity, but disturbances require a bisimulation notion that distinguishes the roles of control and disturbance inputs.
Method
The paper uses alternating approximate bisimulation to construct symbolic models for nonlinear control systems with disturbances and characterizes specialized bisimulation relations for linear systems.
Results
The paper proves that δ–GAS nonlinear control systems with disturbances admit AεA-bisimilar symbolic models with arbitrarily small precision, while linear-system models are easily computable.
Takeaways & Limitations
For a control system and specification, controller existence for the original model and symbolic model is equivalent up to resolution ε.
Takeaways & Limitations
The existence result requires incremental global asymptotic stability; an unstable system satisfying the other theorem conditions may admit no AεA-bisimilar countable transition system.
Abstract
from arXiv · showhide
Symbolic models are abstract descriptions of continuous systems in which symbols represent aggregates of continuous states. In the last few years there has been a growing interest in the use of symbolic models as a tool for mitigating complexity in control design. In fact, symbolic models enable the use of well known algorithms in the context of supervisory control and algorithmic game theory, for controller synthesis. Since the 1990's many researchers faced the problem of identifying classes of dynamical and control systems that admit symbolic models. In this paper we make a further progress along this research line by focusing on control systems affected by disturbances. Our main contribution is to show that incrementally globally asymptotically stable nonlinear control systems with disturbances admit symbolic models. When specializing these results to linear systems, we show that these symbolic models can be easily constructed.
1. Introduction
Symbolic models reduce controller-synthesis complexity by replacing equivalent continuous states with simpler state representations. This paper extends symbolic-model results to incrementally globally asymptotically stable control systems with exogenous disturbances using alternating approximate bisimulation.
- Motivation: Symbolic models replace equivalent states by symbols, often yielding finite-state abstractions on which supervisory-control and algorithmic-game-theory methods can synthesize controllers.These abstractions are typically simpler because they contain fewer states than the original systems.
- Research gap: Prior symbolic-model results covered dynamical or control systems without exogenous disturbances, whereas realistic physical processes often include disturbance inputs.
- Contribution: The paper shows that incrementally globally asymptotically stable nonlinear control systems affected by exogenous inputs admit symbolic models.
- Contribution: Alternating approximate bisimulation distinguishes control inputs from disturbance inputs so synthesized control strategies transfer robustly to the original system.Ordinary approximate bisimulation does not capture the different roles of control and disturbance inputs.
2. Control systems and stability notions
The paper formalizes control systems with control and disturbance inputs, measurable locally essentially bounded signals, continuous dynamics, and unique trajectories. It then introduces forward completeness and incremental global asymptotic stability as the key stability framework.
- Control systems: A control system uses R^n as its state space, input space U × V, and continuous dynamics satisfying a compact-set Lipschitz condition.U is the control-input space and V is the disturbance-input space.
- Control systems: Trajectories are absolutely continuous solutions of the dynamics, and the system’s state at time τ is uniquely determined by the initial state and input.The stated assumptions on the dynamics ensure existence and uniqueness of trajectories.
- Forward completeness: Forward completeness means every trajectory is defined on an interval extending to infinity, with radial-growth conditions characterizing this property under compact inputs.
- Stability notions: Incremental global asymptotic stability requires trajectories under the same input to converge according to a class-KL bound on their initial-state distance.The defining inequality is ∥x(t, x1, w) − x(t, x2, w)∥ ≤ β(∥x1 − x2∥, t).
- Stability notions: For forward-complete systems with compact input sets, δ–GAS is equivalent to existence of a δ–GAS Lyapunov function.The paper notes that the trajectory inequality can therefore be characterized through dissipation inequalities.
3. Symbolic models and approximate equivalence notions
The paper models control systems as alternating transition systems and introduces approximate equivalence notions that distinguish control choices from disturbance responses. An example shows why ordinary approximate bisimulation can fail for disturbance-robust control, motivating alternating approximate bisimulation.
- Alternating transition systems: Alternating transition systems model control synthesis as a two-player arena in which control labels are chosen against disturbance labels.They represent system dynamics through labeled transitions, with states as nodes and transitions as possible evolutions.
- Alternating transition systems: Sampling trajectories over a chosen duration τ yields a sub-transition system used as a time-discretized representation of the control system.The sampled system has continuous states as outputs and uses the state identity map as its output function.
- Approximate equivalence: Approximate bisimulation relaxes exact output matching by requiring outputs to remain within a prescribed precision ε.The relation connects transition sequences in both systems while allowing metric output discrepancies bounded by ε.
- Alternating and approximate bisimulations: In the example, ordinary approximate bisimulation certifies a symbolic model, but its control strategy does not ensure the reachability objective under all disturbances.The control label a3 guarantees reaching R2 ∪ R3 robustly, whereas a2 does not, even though ordinary approximate bisimulation does not distinguish them.
- Alternating and approximate bisimulations: Alternating ε-approximate bisimulation replaces ordinary matching with quantified control–disturbance responses in both directions.Its conditions require matching a control choice, then responding to every disturbance choice with a corresponding disturbance response while preserving the relation.
4. Existence of symbolic models
The paper constructs countable symbolic models for δ–GAS nonlinear control systems with disturbances, using sampling and quantization while preserving alternating approximate bisimilarity. It also shows that unstable systems may lack countable symbolic models and that bounded reachable sets ensure countability.
- Under δ–GAS and compact input sets, a countable transition system exists that is AεA bisimilar to the sampled control system for any desired precision.
- An unstable scalar system provides a counterexample showing that countable symbolic models need not exist without δ–GAS.The example establishes failure of AεA bisimilarity for every sampling time and countable candidate system at some precision.
- The proof proceeds by defining the symbolic transition system, establishing countability, and proving AεA bisimilarity under δ–GAS.
- The construction samples trajectories and quantizes state and input spaces using parameters τ, η, and µ to obtain Tτ,η,µ(Σ).The resulting model extracts countable states and labels while targeting a prescribed approximation precision.
- Bounded reachable sets guarantee countability, and bounded state spaces additionally make the proposed transition system finite.
5. Linear control systems
For linear control systems, the paper gives a more easily constructible symbolic model whose disturbance and control labels can be separated because of linearity. Under asymptotic stability and suitable parameters, this model is alternating approximately bisimilar to the sampled system.
- The linear symbolic model is countable and can be constructed using reachable-set approximations, with numerical errors incorporated into its transition condition.
- Linearity makes the symbolic construction easier and allows disturbance labels to be defined independently from control labels.The distinction from the nonlinear construction follows from the linear system structure.
- The model differs from the nonlinear construction mainly in the definition of its label sets, while the transition relations are substantially equivalent.
- For asymptotically stable linear systems satisfying condition (5.5), Tτ,η,µ(Σ) is AεA bisimilar to Tτ(Σ).
- The symmetric construction also yields (Aτ, A)–(Bτ, B)–AεA bisimilarity, which is relevant for symbolic models of infinite-state games.
6. Illustrative Example
The example constructs a symbolic model for a stable direct-current motor with bounded control and disturbance inputs, then uses it to solve disturbance rejection. The model is AεA bisimilar to the original transition system with ε = 0.5, and the synthesized controls solve the original problem.
- Problem: The motor problem seeks a memoryless control strategy ensuring angular velocity x2 exceeds 0.1 at t = 5 for every initial state and disturbance.The state, control, and disturbance domains are X = [0, 0.6] × [0, 0.6], U = [0.3, 0.7], and V = [−0.02, 0.02].
- Symbolic model: Choosing ε = 0.5, τ = 5, µ = 0.3, and η = 0.15 yields a symbolic transition system AεA bisimilar to the original system.The construction uses outer approximations of control- and disturbance-induced reachable sets and their associated label sets.
- Symbolic model: The resulting nine-state model uses four control labels and three disturbance labels to represent the motor's transitions.Its transition relation records successor states for label pairs, while entries outside X are omitted.
- Controller synthesis: The symbolic model supports disturbance-rejection synthesis by identifying control labels that reach target states for every disturbance label.The synthesized control labels can be converted into control inputs for the original controllable linear system.
- Controller synthesis: The obtained control inputs solve the disturbance-rejection problem on the original linear system.This follows from the transition-system definition and the established correspondence between the symbolic and original systems.
7. Discussion
The discussion extends symbolic-model results to disturbed nonlinear control systems and emphasizes alternating approximate bisimulation as the appropriate correspondence. The resulting equivalence supports controller synthesis transfer between symbolic and original systems up to a chosen resolution.
- Main conclusions: The paper establishes AεA-bisimilar symbolic models for δ-GAS nonlinear control systems with disturbances, with arbitrarily small precision ε.For asymptotically stable linear systems, the models are also easily computable and satisfy a stronger parameterized bisimulation result.
- Main conclusions: Alternating approximate bisimulation distinguishes control inputs from disturbance inputs, unlike prior approximate-bisimulation results that could not preserve their different roles.This distinction is necessary because controllers synthesized on an unsuitable symbolic model may not transfer to the original system.
- Extensions: Relative to earlier results, the paper enlarges the systems from linear to nonlinear, allows measurable locally essentially bounded controls, and generalizes simulation to bisimulation.The bisimulation result provides a more accurate description for controller synthesis.
- Implications: Up to resolution ε, a controller exists for the original model if and only if a controller exists for the symbolic model.This equivalence is stated for a given control system and specification.