Source-linked AI summary
Symbolic control of stochastic systems via approximately bisimilar finite abstractions
Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros
TL;DR
Controller synthesis for continuous-time stochastic systems lacks comprehensive finite abstractions suitable for probabilistic models. The paper constructs quantized symbolic models under probabilistic incremental stability, relates them to probabilistic bisimulation notions, and demonstrates synthesis for linear temporal logic specifications. The resulting framework supports finite approximately bisimilar models on bounded state sets, with state-set cardinality identified as the main limitation.
Problem
Continuous-time continuous-space stochastic control systems lack comprehensive finite bisimilar abstractions, despite modeling uncertain cyber-physical systems and motivating automated controller synthesis.
Method
The paper quantizes state and input sets to construct symbolic models for systems satisfying probabilistic incremental input-to-state stability, with ε-approximate bisimulation in moments.
Results
The construction yields finite approximately bisimilar symbolic models on bounded state sets and supports controller synthesis for rich linear temporal logic specifications in two case studies.
Takeaways & Limitations
The framework provides an automated, correct-by-construction route for synthesizing controllers for stochastic control systems from finite symbolic models.
Takeaways & Limitations
The main limitation is the cardinality of the computed symbolic model's state set.
Abstract
from arXiv · showhide
Symbolic approaches to the control design over complex systems employ the construction of finite-state models that are related to the original control systems, then use techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally translate the synthesized schemes back as controllers for the concrete complex systems. Such approaches have been successfully developed and implemented for the synthesis of controllers over non-probabilistic control systems. In this paper, we extend the technique to probabilistic control systems modeled by controlled stochastic differential equations. We show that for every stochastic control system satisfying a probabilistic variant of incremental input-to-state stability, and for every given precision $\varepsilon>0$, a finite-state transition system can be constructed, which is $\varepsilon$-approximately bisimilar (in the sense of moments) to the original stochastic control system. Moreover, we provide results relating stochastic control systems to their corresponding finite-state transition systems in terms of probabilistic bisimulation relations known in the literature. We demonstrate the effectiveness of the construction by synthesizing controllers for stochastic control systems over rich specifications expressed in linear temporal logic. The discussed technique enables a new, automated, correct-by-construction controller synthesis approach for stochastic control systems, which are common mathematical models employed in many safety critical systems subject to structured uncertainty and are thus relevant for cyber-physical applications.
1. Introduction, Literature Background, and Contributions
The paper addresses the lack of comprehensive finite bisimilar abstractions for continuous-time stochastic control systems by extending symbolic control methods to probabilistic models. It establishes approximate abstractions under a probabilistic incremental stability condition and demonstrates controller synthesis for linear temporal logic specifications.
- Finite symbolic models support finite-state reactive synthesis while preserving traces up to precision ε through approximate bisimulation.
- Existing abstraction results for stochastic systems are limited, leaving continuous-time continuous-space stochastic control systems without comprehensive finite bisimilar abstractions.
- For any ε > 0, systems satisfying probabilistic incremental input-to-state stability admit ε-approximately bisimilar symbolic models in the sense of moments.
- The construction uses finite-state synthesis and supports controller refinement between symbolic and original stochastic systems.
- Two case studies synthesize controllers for nonlinear stochastic control systems under rich linear temporal logic specifications.
2. Stochastic Control Systems
The paper formalizes stochastic control systems as systems with continuous states, inputs, drift, diffusion, and solution processes driven by Brownian motion. Lipschitz assumptions ensure existence and uniqueness of the resulting processes.
- State-space boxes are approximated by finite grids whose points provide a finite covering when the grid spacing does not exceed the box span.
- A stochastic control system consists of a state space, input set, admissible input functions, drift function, and diffusion function.
- The drift is Lipschitz in states and inputs, while the diffusion satisfies a corresponding Lipschitz assumption.
- Solution processes are generated from initial conditions and input curves through the stochastic dynamics driven by Brownian motion.
- The model may begin from a random initial condition measurable with respect to the initial sigma-algebra.
- The stated assumptions on drift and diffusion guarantee existence and uniqueness of solution processes.
3. A Notion of Incremental Stability
The paper introduces δ-ISS-Mq to quantify incremental stability of stochastic control systems in moments and characterizes it through Lyapunov functions. These conditions support trajectory bounds and abstraction construction, including numerically checkable criteria for linear systems.
- δ-ISS-Mq generalizes incremental input-to-state stability to stochastic systems by bounding expected qth-moment trajectory differences over time.
- A δ-ISS-Mq Lyapunov function yields δ-ISS-Mq for the stochastic control system.
- The resulting trajectory bound combines exponentially decaying initial mismatch with an input-mismatch term.
- For linear stochastic systems, a linear matrix inequality provides a numerically solvable sufficient condition for constructing the Lyapunov function.
- The stability analysis also bounds distances between stochastic trajectories and trajectories of the corresponding noise-free system.
4. Symbolic Models
The paper represents stochastic control systems and symbolic abstractions as transition systems with states, inputs, transitions, outputs, and output maps. Approximate bisimulation requires mutual approximate simulation with output discrepancies bounded by ε.
- A system is defined by states, initial states, inputs, a transition relation, outputs, and an output map.
- Systems are finite when their state sets are finite and deterministic when each state-input pair has exactly one successor.
- An ε-approximate simulation relation matches initial states, bounds related outputs within ε, and preserves corresponding transitions.
- An ε-approximate bisimulation relation requires approximate simulation in both directions.
- When ε = 0, approximate relations reduce to exact simulation or bisimulation relations.
5. Symbolic Models for Stochastic Control Systems
The paper constructs finite symbolic models for stochastic control systems under δ-ISS-Mq conditions, using state and input quantization to obtain ε-approximate bisimilarity. It also develops probabilistic abstraction results supporting controller synthesis and temporal-logic specifications.
- Symbolic-model construction: A stochastic control system admitting a δ-ISS-Mq Lyapunov function can be related to a finite system that is ε-approximately bisimilar for any ε > 0.The construction uses a metric-system representation of the stochastic control system and quantization parameters for the abstraction.
- Symbolic-model construction: Quantizing bounded state and input sets provides a simple construction of the symbolic abstraction, with precision governed by sampling and quantization parameters.The lower bound on ε can decrease with sampling time, Lipschitz constants, or an appropriate choice of δ-ISS-Mq Lyapunov function.
- Symbolic-model construction: Alternative δ-ISS-Mq conditions can yield symbolic models with fewer states or a better precision bound for a fixed sampling time.The paper contrasts the Lyapunov-function-based construction with a formulation using comparison functions β and γ.
- Probabilistic abstraction relations: The abstraction results establish matching state runs between sampled stochastic systems and symbolic models, including probabilistic approximate bisimulation relations.A point-wise-in-time relation is presented for LTL specifications whose satisfiability can be checked at single time instances, such as next and eventually.
- Assumptions and scope: The main results require δ-ISS-Mq assumptions, while a finite-horizon alternative is computationally more tractable and does not require stochastic bisimulation functions.For systems that are not δ-ISS-Mq, the paper notes that sufficient abstractions may preserve refinements in one direction but lose the converse controller-existence guarantee.
6. Case Studies
The case studies apply the symbolic-abstraction method to noisy nonlinear and linear control models, synthesizing controllers for temporal specifications and evaluating their refinements empirically and probabilistically.
- Experimental setup: The experiments use finite abstractions computed with Pessoa for piecewise-constant inputs of duration τ.The implementation assumes finite input sets and uses µ = 0 in the relevant abstraction conditions.
- Nonlinear model: For the nonlinear pendulum model, the system is analyzed on D = [−1, 1] × [−1, 1] and shown to be δ-ISS-M2 through a Lyapunov function.The reported parameters include κ = 0.7691 and ρ(r) = 8.76r.
- Nonlinear model: With τ = 3 and ε = 0.085, the nonlinear abstraction has 370881 states and 7 inputs, while Theorem 5.3 is less conservative than Theorem 5.1.The corresponding quantization parameter is η = 0.0033.
- Nonlinear model: The synthesized nonlinear controller sequentially visits W1 and W2, then returns to W1 and remains there under the specified LTL formula.Controller synthesis takes 3.02 seconds, and empirical distances are below ε = 0.085, consistent with conservative Lyapunov bounds.
- Linear model: The DC-motor abstraction contains 1002001 states and 11 inputs, requires ε = 1, and takes 148.092 seconds to compute.Theorem 5.3 cannot be applied for τ = 0.01 because its condition is not fulfilled.
- Linear model: For the linear DC motor, refinement satisfies the inflated LTL specification with probability at least 70% over the horizon {0, 0.01, 0.02, ···, 1} seconds.The target formula is 3^2W ∧ 2Z, and the refined formula is 3^2W^1 ∧ 2Z^1.
7. Conclusions
The paper concludes that stochastic sampled-data systems with suitable δ-ISS-Mq Lyapunov functions admit finite approximately bisimilar symbolic models that support complex temporal-logic controller synthesis. It identifies abstraction-state cardinality as the main limitation and notes ongoing work on extensions.
- Conclusions: Systems with a δ-ISS-Mq Lyapunov function and compact initial-state set admit finite approximately bisimilar symbolic models.The approximation may be expressed in moments or probability.
- Conclusions: The symbolic models support controller synthesis for complex specifications expressed in linear temporal logic or automata on infinite strings.
- Limitations and future work: The main limitation is the cardinality of the computed symbolic model's state set.The authors report investigating specification-guided, differentially flat, and non-uniform quantization approaches, alongside extensions to general stochastic hybrid systems.
9. Appendix
The appendix supplies proofs and technical bounds supporting the Lyapunov-based stochastic abstraction results. It uses Itô calculus, Gronwall-type arguments, Lipschitz conditions, and explicit system-parameter estimates.
- Lyapunov-function proofs: The appendix verifies Lyapunov-function properties using differentiability, mean-value arguments, and the definitions of the incremental stability conditions.
- Stochastic estimates: For stochastic systems, the proofs apply Itô's formula, Jensen's inequality, Lipschitz continuity of diffusion terms, and Gronwall's inequality.
- Explicit estimates: The technical results yield more explicit bounds in terms of system parameters.