Compositional Approximately Bisimilar Abstractions of Stochastic Interconnected Systems

1 Introduction

• Monolithic abstraction can become computationally intractable as interconnected systems grow, while compositional methods exploit subsystem modularity.The paper identifies controller synthesis for interconnected stochastic systems as a remaining challenge and targets bidirectional relations, which support refinement with quantifiable error bounds.Source: §1 · p. 2
• This version extends preliminary results in [25] to stochastic systems and adds detailed proofs, examples, and a case study.Source: §1 · p. 2
• The framework uses approximate composition and δ-ISS-Mq to extend subsystem-level stochastic (alternating) bisimulation to the global interconnected system.This strengthens one-directional simulation results to a bidirectional guarantee that supports controller refinement with quantified error.Source: §1 · pp. 2–3
• A tighter upper bound on the qth-moment distance between noisy and noise-free trajectories holds under a mild moment inequality on the diffusion term.Source: §1 · p. 3
• The comparative analysis reports reduced abstraction computation time for large-scale systems and validates the approach in a ten-room temperature-regulation case study.Source: §1 · p. 3
• Compared with [29], the paper proves the converse direction under δ-ISS; compared with, it gives a bidirectional qth-moment guarantee under approximate composition.Its Lyapunov-free noisy-to-noise-free bound covers q = 1, unlike the cited Lyapunov-based bound in [36, Lemma 3.8], stated for q ≥2.Source: §1 · p. 3

2 Preliminaries and Problem statement

• Preliminaries establish pseudometrics, random-variable and signal norms, and class K, K∞, L, and KL functions used in subsequent definitions.A pseudometric is symmetric, vanishes on identical points, and satisfies the triangle inequality.Source: §2 · p. 3

2.1 Discrete-time stochastic control systems (DT-SCS)

• A DT-SCS has external and internal inputs, a drift map, and bounded i.i.d. noise with specified mean and covariance.The noise values lie in a bounded set containing zero.Source: §2.1 · p. 3

2.2 Incremental Input-to-State Stability in qth-moment for DT-SCS

• The δ-ISS-Mq property bounds qth-moment incremental behavior using class KL and K∞ functions and a constant; for noise-free systems it reduces to standard δ-ISS.The noise-free reduction uses q = 1 and ψ = 0.Source: §2.2 · p. 4

2.3 DT-SCS as a gMDP

• A DT-SCS is represented as a gMDP whose stochastic kernel gives the successor-state distribution induced by the noise, with admissible inputs ensuring successors remain in the state space almost surely.The output set is the state space and the output map is the identity.Source: §2.3 · pp. 4–5

2.4 Noise-free system as Transition system

• The noise-free system is represented as a transition system with a successor relation; admissible inputs require a nonempty successor set contained in the state space.Its output set is the state space with the identity output map.Source: §2.4 · p. 5

2.5 Approximate (alternating) stochastic bisimulation relations

• When R pairs an Lq random variable with a state, the successor condition is a deterministic moment bound by ε, so ϱ = 0 whenever it holds; bisimilarity requires simulation both ways.The lifted relation uses a joint coupling in which related successors occur with probability at least 1−ϱ.Source: §2.5 · pp. 6–7
• The introduced approximate bisimulation definitions allow input-choice mismatch and successor matching in probability, recovering prior notions under specified parameter choices.For Definition 6, µ = 0 and ϱ = 0 recover, while µ = ∞ and ϱ = 0 cover; Definition 7 recovers when µ = ∞ and ϱ = 0.Source: §2.5 · p. 7

2.6 Interconnections among DT-SCS and Ξ-compatibility composition

• Interconnected stochastic subsystems are composed through neighbor outputs and internal inputs, with the global transition kernel formed from local kernels under conditional independence.The construction assumes subsystem transitions are conditionally independent given the current state and external and internal inputs.Source: §2.6 · pp. 8–9

2.7 Problem formulation

• The proposed problem is to construct a scalable deterministic abstraction preserving stochastic (alternating) bisimulation with a large-scale interconnected system, using subsystem relations and q-th-moment incremental input-to-state stability.This bottom-up approach first relates each stochastic subsystem to its noise-free counterpart so behavioral guarantees on the deterministic abstraction can transfer to the global system.Source: §2.7 · p. 10

3 On the distance between the noisy and noise-free system trajectories

• A diffusion-moment condition yields a tighter upper bound on noisy-to-noise-free trajectory distance than direct δ-ISS-Mq application.The bound uses δ-ISS and δ-ISS-Mq estimates together with a bound on the diffusion term; the drift is assumed affine in the state.Source: §3 · pp. 11–12
• For q = 1, the target distance is especially relevant because existing δ-ISS Lyapunov-function approaches typically do not handle it.The construction constrains the noise magnitude at each time step; Figure 2 distinguishes noise effects from deviations between noisy and noise-free trajectories.Source: §3 · p. 11, Figure 2 · p. 11
• When the Lemma 1 bound satisfies Bϑ ≤ ϑ^q for all k, the output-distance relation defines approximate stochastic bisimulation with the noise-free system.The relation bounds the qth-moment output distance by ϑ.Source: §3 · p. 14
• Under the corresponding bound condition, the same relation establishes approximate alternating stochastic bisimulation between the stochastic system and its noise-free counterpart.Theorem 2 uses the relation defined in Theorem 1.Source: §3 · p. 14
• After establishing these relations, the analysis proceeds with the noise-free transition system, carrying the quantified error ϑ into compositionality results.This shifts the remaining analysis from stochastic kernel coupling to direct matching of transition-system successors.Source: §3 · p. 15

4 Compositional bisimilar abstractions for interconnected transition systems

• The framework relates Ξ-compatible composition to the more conservative composition with ¯Ξ ⩾ Ξ and gives conditions for preserving approximate bisimulation between them.These preservation conditions support extending local relations from noise-free subsystems to the global interconnected system.Source: §4 · p. 15

4.1 Assessing Conservatism in Interconnected Systems with δ-ISS Property and Varying Approximate Composition Parameters

• Under δ-ISS, increasing approximate composition parameters can be bounded by an ε-approximate bisimulation relation between the two composed systems.The result establishes symmetric approximate bisimilarity; the alternating version is also symmetric under its stated condition, without a stability requirement.Source: §4.1 · pp. 16–17

4.2 Approximate (Alternating) Bisimilar Composition of the Global noise-free subsystems

• Local approximate bisimulation and alternating-bisimulation relations are preserved under the stated conditions when composing the noise-free subsystems into global systems.The results give compositional extensions for both approximate bisimulation and approximate alternating bisimulation.Source: §4.2 · pp. 19–20

4.3 Approximate Stochastic (Alternating) Bisimilar Relation between the Global Interconnected Stochastic system and noise-free system

• Under the stated local δ-ISS-Mq and stochastic-bisimilarity conditions, the interconnected stochastic system is approximately stochastically bisimilar to its noise-free counterpart.The result is stated for the global system and its noise-free composition.Source: §4.3 · p. 20
• Local approximate stochastic bisimulations compose into a global relation between the interconnected stochastic system and its noise-free counterpart, with parameters (ϑ, 0, 0).The proof uses a product relation and coupling, with the δ-ISS-Mq property handling internal-input mismatch; the argument establishes the relation in both directions.Source: §4.3 · p. 21
• The analogous composition result holds for approximate stochastic alternating bisimulation, yielding a global relation with parameters (ϑ, 0, 0).The proof adapts the coupling argument to the alternating input-quantifier order, choosing identical inputs on both sides.Source: §4.3 · pp. 21–22

4.4 Approximate Stochastic (Alternating) Bisimilar Relations for the Global Interconnected Stochastic System and its noise-free abstraction.

• Transitivity extends the global stochastic bisimulation to the symbolic abstraction of the noise-free system, combining the global and abstraction approximation parameters.The corollary invokes the noise-free transition-system relation with parameters (2ε, µ) and transitivity; the supplied proof passage does not show the full resulting parameter expression.Source: §4.4 · p. 22
• The alternating-bisimulation corollary likewise relates the global stochastic system to its abstraction with parameters (2ε+ϑ, µ).It follows by applying transitivity to the alternating-bisimulation results for the stochastic system and the noise-free transition system.Source: §4.4 · p. 23

5.1 Model description and control objective

• Each room is modeled as a noisy subsystem with neighboring room states as internal inputs and two heaters whose joint input excludes both being on simultaneously.Source: §5.1 · pp. 23–24
• The ten-room control objective is to keep mean room temperatures within S = [18, 21.8]10; the stated guarantee covers the mean, not probabilistic safety.The reported safety controller’s mean trajectories remain within the safe region over 10,000 runs.Source: §5.1 · p. 24
• The noisy subsystem’s bisimulation relation parameter is ϑ = 0.908, almost 45% tighter than the δ-ISS-Mq upper bound.Source: §5.1 · p. 24
• Local symbolic abstractions are built by quantizing subsystem state spaces and evaluating successor maps at quantized states.The reported relation study uses nx = 190 discretized cells per subsystem.Source: §5.1 · p. 24

5. Case study: Temperature Control for Multi-room Building

• 1.621 seconds compositionally versus 343 seconds monolithically for the ten-room abstraction at nx=6.The compositional total includes less than 0.341 seconds for composing the global abstraction from local abstractions.Source: §5.1 · pp. 24–25, Table 2 · p. 24

5.2 Case study with Multi-room Building in Circular Cascade Interconnection

• From eight rooms onward, computation time is significantly reduced compositionally, while the monolithic approach fails to converge beyond ten rooms.The comparison concerns circularly interconnected multi-room buildings.Source: §5.2 · p. 25, Table 3 · p. 25

• The framework gives conditions under which approximate (alternating) stochastic bisimulation is preserved when interconnected subsystems are composed into a larger system.The conclusion reports smaller relational conservatism than that added by the δ-ISS-Mq property.Source: §6 · p. 25
• Compositional abstraction reduces computation time relative to monolithic abstraction for high-dimensional systems with finer discretization and for large-scale systems.Source: §6 · pp. 25–26
• Numerical results demonstrate safety in mean for the proposed framework.Source: §6 · p. 26

• If ∥A∥ < 1, the linear system satisfies δ-ISS-Mq for q ∈ N, with characterizing functions given by Theorem 9.The system has state x, external and internal inputs, and an i.i.d. noise sequence w.Source: §A.1 · p. 28
• The proof tracks the difference between two trajectories at the next time step and rewrites that difference explicitly.Source: §A.1 · p. 28
• Minkowski inequalities are applied to bound trajectory differences, including the noise term.Source: §A.1 · p. 28

• Under Assumption 2 and the stated contraction condition, the nonlinear system satisfies δ-ISS-Mq for q ∈ N.Source: §A.2 · p. 29
• The proof bounds the difference between two trajectories using Assumption 2 and Minkowski’s inequality.Source: §A.2 · p. 29
• For trajectories driven by the same noise realization, the δ-ISS-Mq bound has the same β and γ functions but ψ = 0.Source: §A.2 · p. 29

A.3 Verification procedure for Assumption 1

• Choose λ so the target bound is strictly positive whenever ψ > 0.The procedure selects λ from an interval determined by q.Source: §A.3 · p. 30
• Bound the noise-combination term for the applicable model class; stationarity and compactness make the bound independent of k.The Lipschitz nonlinear case uses a bound on g over compact X and the noise moment.Source: §A.3 · p. 30
• Set R to the supremum of the noise-combination bounds, which is finite under compactness of X and a bounded noise moment.R is the finite, k-independent envelope used in the subsequent feasibility check.Source: §A.3 · p. 30
• Construct the concave majorant using a log function that dominates r on [0, R].The procedure states that concavity of log(1 + ·) gives the required domination.Source: §A.3 · p. 30
• Confirm Assumption 1 for all k; if the inequality fails, adjust λ or reduce R and repeat.The text suggests shrinking X or improving the Lipschitz or noise-moment estimates to reduce R.Source: §A.3 · p. 30