Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against $\omega$-Regular Specifications

1. Introduction

• Discretization-based verification and synthesis can have complexity exponential in state-space dimension, while compositional abstraction methods instead build system abstractions from subsystem abstractions.The introduction also notes discretization-free barrier-certificate approaches, including work on finite-time LTL specifications and stochastic switched systems.Source: §1 · pp. 1–2
• Compositional dissipativity conditions combine subsystem control sub-barrier certificates into certificates for interconnected stochastic systems, supporting switching policies for ω-regular specifications represented by deterministic Streett automata.The specification is decomposed into simpler tasks, each with subsystem certificates and local policies.Source: §1 · p. 2
• ADMM jointly searches for subsystem certificates and local policies while enforcing compositionality, replacing parameter selection and a posteriori checks with smaller optimization subproblems.For polynomial dynamics, the approach pairs ADMM with SOS optimization; the paper demonstrates it on a 300-room circular-building temperature network.Source: §1 · pp. 2–3
• Against [ALZ22], the paper presents a potentially less conservative dissipativity approach with an LMI compositionality condition, infinite-time guarantees, and an ADMM alternative to post-hoc checking.It also states that it does not require an additional assumption used in [ALZ22].Source: §1 · pp. 2–3
• Compared with [JSZ20], the paper treats stochastic systems and general ω-regular specifications rather than non-stochastic systems and deterministic co-Büchi specifications.It also contrasts its discrete-time framework with continuous-time approaches in [NSZ20b] that use sum-type small-gain conditions and require nearly linear subsystem behavior.Source: §1 · p. 3

2.1. Preliminaries.

• The paper models probability with a sample space, an event sigma-algebra, and a probability measure, and identifies Borel spaces and measurable maps for its system definitions.A random variable induces a probability measure on its measurable state space.Source: §2.1 · p. 3

2.2. Notations.

• Notation defines real-number sets, vector and matrix operations, norms, Cartesian products, set complements, power sets, and logical truth values.For example, R^n denotes real space of dimension n, and the matrix Frobenius norm is written ∥A∥F.Source: §2.2 · p. 3

2.3. Discrete-Time Stochastic Control Systems.

• A discrete-time stochastic control system is formalized by state, external and internal input spaces, i.i.d. noise, a measurable transition map, and output spaces and maps.The system's evolution is given by a measurable state-transition function.Source: §2.3 · pp. 3–4
• For specified initial states and input sequences, the transition function generates a solution process; external and internal inputs are independent of future noise variables.In the no-internal-input case, the state evolves as x(k + 1) = f(x(k), ν(k), ς(k)).Source: §2.3 · p. 4
• Policies may depend on the full history or be stationary state-feedback maps, and synthesis assumes full-state information for the interconnected system.Internal outputs are retained chiefly to describe subsystem interconnections; the large-scale system itself has identity output map.Source: §2.3 · p. 4

3. Control (Sub-)Barrier Certificates

• A control sub-barrier certificate is a nonnegative function defined for a subsystem with internal inputs and outputs relative to initial and unsafe sets.The section uses subsystem certificates as the building blocks for a certificate of the interconnected system.Source: §3 · pp. 4, 6
• For an interconnected system, a control barrier certificate is defined relative to initial and unsafe sets with constants satisfying β > η, a condition required for meaningful safety guarantees.The same inequality is not necessarily required for subsystem certificates with internal inputs and outputs.Source: §3 · p. 5
• A control barrier certificate provides an upper bound on the probability of reaching an unsafe region and a lower bound on the probability of avoiding it over an infinite horizon.These bounds apply to solution processes starting in the specified initial set under the control policy.Source: §3 · p. 5
• Infinite-horizon guarantees require the certificate to be a nonnegative supermartingale, which can be restrictive; relaxing this with a positive offset permits c-martingales but limits guarantees to finite horizons.The paper proposes constructing large-system certificates from subsystem certificates to address the computational difficulty of direct search.Source: §3 · pp. 5–6

4.1. Interconnected Stochastic Control Systems.

• The network interconnection couples subsystem outputs to internal inputs, and controller synthesis assumes each subsystem has full-state information.The interconnected system's state space is the product of subsystem state spaces.Source: §4.1 · p. 6

4.2. Compositional CBC for Interconnected Systems.

• Sufficient compositional conditions make the sum of subsystem control sub-barrier certificates a control barrier certificate for the interconnected system.Each subsystem must admit a control sub-barrier certificate; the conditions use the interconnection matrix and subsystem parameters.Source: §4.2 · p. 6

4.3. Compositional Certification using ADMM Algorithm.

• ADMM decomposes the compositionality condition into parallel local subproblems and a global problem involving the interconnection matrix.Local and global solutions update the primal and dual variables iteratively; the paper states that the convex objectives guarantee convergence to optimal solutions.Source: §4.2 · p. 7, §4.3 · p. 8

4.4. Computation of CSBC and Control Policy.

• For polynomial subsystem dynamics, SOS optimization searches for polynomial control sub-barrier certificates and corresponding local control policies.The SOS formulation relies on Assumption 4.6, which requires polynomial transition maps.Source: §4.4 · pp. 8–9
• The SOS–ADMM computation assumes polynomial sub-barrier certificates; CEGIS avoids that assumption at the cost of greater computational complexity.The paper notes that CEGIS is an alternative computation method without the polynomial-certificate assumption.Source: §4.4 · p. 9
• Dense interconnection topologies can increase ADMM, LMI, and SOS computational costs, whereas certain sparse topologies can yield linear complexity in subsystem count.The paper states that solving LMI (14) is cubic in the number of subsystems and that sparse patterns can yield linear complexity.Source: §4.4 · p. 9

5. Class of Specifications

• Deterministic Streett automata represent ω-regular properties while retaining the determinism needed for controller synthesis.The paper selects Streett automata because they have the expressive power of nondeterministic Büchi automata, unlike deterministic Büchi automata.Source: §5 · p. 10

5.1. Satisfaction of Specifications by Interconnected Systems.

• The synthesis problem seeks a policy and a probability lower bound for specification satisfaction, despite high system dimension and complex specifications.The proposed response is to compose subsystem certificates and reduce automaton properties to sequential safety tasks.Source: §5.1 · p. 11

5.2. Specification Decomposition.

• The decomposition enumerates partially accepting lassos and converts their finite paths and cycles into consecutive safety tasks.The resulting tasks support barrier-certificate bounds; time spent in ignored self-loops remains accounted for by the certificate construction.Source: §5.2 · p. 12
• Combining safety-task violation bounds yields a lower bound on specification satisfaction, but tracking only finitely visited E states introduces conservatism.The paper notes that this safety-based route ignores the alternative condition of visiting F states infinitely often.Source: §5.2 · pp. 13–14

6.1. Control Policy.

• Tasks sharing a common certificate are grouped so one controller can handle outgoing automaton branches, with a switching automaton selecting the policy.The switching automaton tracks automaton transitions and the successor set associated with each state.Source: §6.1 · p. 14, §6 · p. 14

6.2. Probability Computation.

• Combining safety-task violation bounds gives a lower bound on specification satisfaction by bounding repeated visits to E states.When a finite-cycle safety task admits a certificate, the bound for infinitely repeating that loop is zero; otherwise the guarantee may cover visits to E only at most once.Source: §6.2 · p. 15
• If a safety task lacks a certificate, its lower bound is zero; a nontrivial overall bound requires at least one task with a suitable certificate.Reconstructing the automaton by duplicating E states can extend guarantees to visiting those states at most N times.Source: §6.2 · p. 16
• The guarantee may fall to zero when individual task-violation bounds are near one or trivial, and subsystem count can affect it for nonidentical subsystems.For identical subsystems, the stated upper bound remains unchanged with subsystem count.Source: §6.2 · p. 16

• The model comprises 300 room subsystems with multiplicative noise, and the synthesized controller takes values in [0, 0.6]^n.Source: §7 · pp. 17–18
• The Streett automaton is decomposed into four safety tasks, with the cycle task (q4, q3, q4) prioritized for certificate and policy synthesis.Source: §7 · p. 17
• Figure 5 shows 10 noise-realization trajectories from X2 for a representative room; certificate and local-policy computation takes up to 240 seconds.Source: Figure 5 · p. 18, §7 · p. 19
• ADMM with an SOS formulation yields a fourth-order subsystem control sub-barrier certificate and a corresponding local controller, νi(Ti) = 0.59 − 0.011Ti.Source: §7 · p. 18
• The upper bound on reaching X1 from X0 is 0.0594, while the DSA specification is satisfied with probability 1.Source: §7 · p. 18

8.1. Discussion.

• The approach decomposes DSA specifications into safety properties, so it does not use states in F; reachability certificates may help reduce this conservatism.Source: §8.1 · p. 19

8.2. Conclusion.

• The paper combines topology-informed dissipativity conditions and subsystem certificates with ADMM, SOS computation, and DSA task decomposition, then demonstrates the approach on room-temperature regulation.Source: §8.2 · p. 19

• The nonnegative-supermartingale property of the certificate yields probability bounds via [Kus67, Theorem 12, Chapter II].Source: §9 · p. 21
• Theorem 4.3’s proof establishes the composed certificate’s required bounds and uses coupling-induced internal inputs to verify condition (9).Source: §9 · p. 21
• The SOS multiplier constraints imply subsystem conditions (4)–(6), including the existence of a suitable local control input.Source: §9 · p. 22
• Theorem 6.1 first upper-bounds infinite visits to E, sums probabilities across possible lassos, and uses the result to obtain a lower bound on specification satisfaction.Source: §9 · pp. 22–23
• For each safety task ϑ, Lemma 5.9 supplies ηϑ, an upper bound on reaching its target region from its initial region under νϑ.Source: §9 · p. 22