Source-linked AI summary
Approximately bisimilar symbolic models for nonlinear control systems
Giordano Pola, Antoine Girard, Paulo Tabuada
TL;DR
Continuous differential-equation models are powerful for physical phenomena but less suited to software and hardware interaction, motivating symbolic abstractions. The paper constructs approximately bisimilar symbolic models for incrementally stable nonlinear control systems, with arbitrarily selectable error and finite abstractions for bounded state spaces.
Problem
Differential-equation models are less suitable for describing software and hardware interfacing with physical systems, motivating symbolic models that support unified control analysis and synthesis.
Method
The paper uses approximate bisimulation to construct symbolic abstractions of nonlinear control systems and quantizes inputs for digital control systems under δ–ISS.
Results
Every δ–GAS nonlinear control system admits an approximately bisimilar symbolic model with arbitrarily small designable error; bounded state spaces yield finite models.
Takeaways & Limitations
Approximate bisimulation supports controller synthesis on symbolic models while preserving the desired behavior on the original control system within the approximation error.
Takeaways & Limitations
Constructing the proposed models can require difficult reachable-set or δ–ISS Lyapunov-function computations, and model cardinality grows exponentially with state and input-space dimensions.
Abstract
from arXiv · showhide
Control systems are usually modeled by differential equations describing how physical phenomena can be influenced by certain control parameters or inputs. Although these models are very powerful when dealing with physical phenomena, they are less suitable to describe software and hardware interfacing the physical world. For this reason there is a growing interest in describing control systems through symbolic models that are abstract descriptions of the continuous dynamics, where each "symbol" corresponds to an "aggregate" of states in the continuous model. Since these symbolic models are of the same nature of the models used in computer science to describe software and hardware, they provide a unified language to study problems of control in which software and hardware interact with the physical world. Furthermore the use of symbolic models enables one to leverage techniques from supervisory control and algorithms from game theory for controller synthesis purposes. In this paper we show that every incrementally globally asymptotically stable nonlinear control system is approximately equivalent (bisimilar) to a symbolic model. The approximation error is a design parameter in the construction of the symbolic model and can be rendered as small as desired. Furthermore if the state space of the control system is bounded the obtained symbolic model is finite. For digital control systems, and under the stronger assumption of incremental input-to-state stability, symbolic models can be constructed through a suitable quantization of the inputs.
1. Introduction
Symbolic models abstract continuous control dynamics into models suited to software and hardware interaction, enabling supervisory-control and game-theoretic controller synthesis. This paper extends approximate simulation results to approximate bisimulation for nonlinear systems.
- Symbolic models abstract continuous control systems and provide a unified framework for analyzing physical systems alongside interacting software and hardware.
- Bisimulation reduces complexity by relating states through an equivalence relation that respects system dynamics and induces a quotient system.
- Prior symbolic-model research spans discrete-time, continuous-time, quantized, qualitative-reasoning, and stochastic-automata approaches.
- Approximate bisimulation relaxes exact equivalence, allowing a larger class of control systems to admit symbolic models.
- The paper extends prior one-sided approximate simulation results because failure to synthesize a controller symbolically otherwise says nothing about the original system.
2. Control systems and stability notions
The paper formalizes control systems through trajectories generated by inputs and recalls incremental stability notions that support later symbolic-model results. δ–GAS compares trajectories under common inputs, while δ–ISS also accounts for differing inputs.
- A control system is formalized as a state space, input space, admissible input signals, and a continuous vector field satisfying a local Lipschitz condition.
- Trajectories are locally absolutely continuous solutions of ẋ(t) = f(x(t), u(t)) for almost all times, with existence and uniqueness ensured by the assumptions on f.
- δ–GAS requires forward completeness and bounds the distance between trajectories from different initial states under the same input by a KL function.
- δ–ISS bounds trajectory differences using both initial-state separation and the infinity-norm difference between input signals.
- δ–ISS implies δ–GAS, but the converse does not hold in general.
- For compact input spaces, δ–GAS is equivalent to existence of a δ–GAS Lyapunov function, and δ–ISS has an analogous Lyapunov characterization under stated input conditions.
3. Approximate bisimulation
The paper represents a control system as a metric transition system whose transitions encode reachable states under labeled inputs. Approximate bisimulation then relates this infinite model to countable or finite abstractions while tolerating output error ε.
- A transition system consists of states, labels, a transition relation, an output set, and an output function.
- A transition system is countable when its states and labels are countable, and finite when both sets are finite.
- The transition system T(Σ) uses states and outputs in R^n, labels from admissible inputs, and transitions determined by states reached after some duration under an input.
- The metric transition system T(Σ) preserves the control system’s information through its transition relation but has an infinite state space.
- An ε-approximate bisimulation relation matches transitions in both directions while allowing corresponding outputs to differ by at most ε.
4. Approximate bisimilar symbolic models
The paper constructs a countable symbolic model by sampling trajectories, quantizing states and inputs, and selecting transitions within a prescribed radius. Under δ–GAS and suitable parameter choices, this model is ε-bisimilar to the sampled control system; unstable systems may lack countable symbolic models.
- Symbolic-model construction: Sampling at τ and quantizing states with η and inputs with µ yields a countable symbolic transition system, finite when the control-system state space is bounded.The transition relation connects quantized states to sampled successors within η/2; η and µ represent state- and input-space quantization parameters.
- Symbolic-model construction: Reachable sets are approximated by countable sets of representative states and associated control labels, with endpoint error bounded by µ.For each reachable state approximation, a label is selected whose trajectory endpoint lies within µ/2, producing the bound ∥x(τ, q, l1) −x(τ, q, l2)∥≤µ.
- Approximate bisimulation: Theorem 4.1 states that a δ–GAS control system has an ε-bisimilar symbolic model Tτ,η,µ(Σ) when τ, η, and µ satisfy the theorem’s inequality.For δ–GAS systems, sufficiently large τ and sufficiently small η and µ ensure that the required condition can be met.
- Approximate bisimulation: The bisimulation proof relates each continuous state x to a quantized state q whenever their distance is at most ε and verifies matching transitions in both systems.The relation is R={(x,q):∥x−q∥≤ε}; the proof uses δ–GAS and the quantization bounds to preserve this relation after transitions.
- Scope and limitations: Global δ–GAS is a substantive scope condition: unstable systems such as f(x)=x generally admit no countable ε-bisimilar symbolic model.For f(x)=x, distances between distinct related states grow as e^(τk), eventually violating the ε-closeness condition required by approximate bisimulation.
- Scope and limitations: The general symbolic-model construction is difficult because it requires computing reachable sets; digital control systems permit an alternative based on input quantization.The paper identifies reachable-set computation as the construction bottleneck and motivates a separate quantized-input construction for digital systems.
5. Digital control systems
For digital control systems with piecewise-constant inputs, the paper constructs countable symbolic models by quantizing control inputs and proves their approximate bisimilarity under δ–ISS.
- Digital-control setting: Digital control systems use piecewise-constant control signals, with inputs drawn from a hyperrectangle containing the origin.For a sampling period τ, the considered input class consists of signals constant over sampling intervals.
- Symbolic construction: The continuous transition system is approximated by a countable model whose states use η-resolution and whose inputs are quantized with precision µ.The symbolic construction uses Q2 and L2, with transitions based on the sampled system trajectory and an η/2 proximity condition.
- Symbolic construction: Unlike the earlier construction, input-label selection does not require prior knowledge of the system’s reachable set.The transition computation can be performed analytically or numerically, supporting symbolic-model construction from sampled trajectories.
- Approximate bisimulation: The δ–ISS assumption therefore provides the stated link between digital control systems and symbolic models.The proof concludes that the relation satisfies the approximate bisimulation conditions.
- Approximate bisimulation: The proof uses the relation R={(x,q): ||x−q||≤ε} and δ–ISS bounds to establish the required matching transition conditions in both directions.The construction ensures state coverage, while the inequalities preserve the relation after transitions.
6. Symbolic control design for a pendulum
The paper applies its symbolic-model construction to a bounded, piecewise-constant-input pendulum and synthesizes discrete control strategies for alternating periodic motions. Approximate bisimulation transfers the synthesized behavior to the continuous pendulum with a bounded error.
- Pendulum model: The pendulum model describes angular position and velocity under torque input, with gravity, rod length, mass, and friction specified explicitly.The example restricts inputs to U=[−1.5,1.5] and analyzes the bounded state subset X=[−1,1]×[−1,1].
- Pendulum model: A Lyapunov-function argument establishes that the pendulum system is δ–ISS on the considered setting.The construction uses bounds on the Lyapunov function and derives the required comparison functions and decay condition.
- Symbolic model: For ε=0.25, the example chooses η=0.4, τ=2, and µ=1.5·10^-4 to construct the symbolic transition system.Its states form a five-by-five η-grid, its labels are the µ-quantized inputs, and transitions are obtained by numerical trajectory integration.
- Controller synthesis: The controller objective alternates between periodic motions P1 and P2, represented by cycles through specified pendulum states.P1 cycles between (−η,0) and (0,0), whereas P2 cycles between (−η,0) and (η,0).
- Controller synthesis: A simple search on the symbolic model, or standard supervisory-control and game-theoretic methods, produces strategies for P1 and P2.The overall specification is enforced by concatenating trajectories associated with P1, P1, P2, P1, and P1.
- Controller synthesis: 0.25-bisimilarity guarantees that the synthesized controller enforces the desired behavior on the continuous pendulum with error at most 0.25.The reported evolution keeps the state variables within the intervals corresponding to the desired precision at the sampled times.
7. Discussion
The paper generalizes symbolic-model results through approximate bisimulation and develops constructions for linear and quantized control systems. It also identifies computational limitations, especially parameter selection and exponential model growth.
- Simulation/bisimulation: The paper strengthens prior work by allowing any measurable control input and guaranteeing approximate bisimulation rather than approximate simulation.These results follow the simulation/bisimulation research line and generalize the earlier construction.
- Linear systems: For linear systems, explicit expressions for β and γ simplify the search for τ, η, and µ and support symbolic-model construction with non-constant inputs.Reachable sets can also be approximated by polytopes to any desired precision ν.
- Quantized control systems: Under δ–ISS, the results ensure a lattice approximating the reachable-state set independently of system parameters and the input set.This contrasts with earlier finite-abstraction conditions tied to those parameters and inputs.
- Qualitative reasoning and stochastic automata: Qualitative-reasoning and stochastic-automata abstractions provide completeness in one direction, whereas approximate bisimulation supplies the converse matching property under δ–ISS.Thus, symbolic trajectories and control-system trajectories can be related in both directions within the approximation.
- Limitations and future work: Effective construction remains challenging because finding δ–ISS Lyapunov functions is hard and the sizes of Q2 and L2 grow exponentially with state and input dimensions.The paper proposes numerical tools and on-the-fly verification techniques as possible ways to address these issues.