Compositional Design of Safety Controllers for Large-Scale Stochastic Hybrid Systems

Abolfazl Lavaei; Behrad Samari; Mahdieh Zaker; Omid Akbarzadeh

arxiv: 2409.10018 · v3 · submitted 2024-09-16 · 📡 eess.SY · cs.SY

Compositional Design of Safety Controllers for Large-Scale Stochastic Hybrid Systems

Mahdieh Zaker , Omid Akbarzadeh , Behrad Samari , Abolfazl Lavaei This is my paper

Pith reviewed 2026-05-23 21:11 UTC · model grok-4.3

classification 📡 eess.SY cs.SY

keywords compositional synthesissafety controllersstochastic hybrid systemscontrol barrier certificatessmall-gain conditionsinterconnected networkssum-of-squares optimizationlarge-scale systems

0 comments

The pith

Compositional small-gain conditions combine subsystem barrier certificates into network-level safety controllers for stochastic hybrid systems.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a compositional method for synthesizing safety controllers in large networks of stochastic hybrid systems that include both continuous evolution and instantaneous jumps. It defines an augmented scheme for each subsystem and introduces augmented control sub-barrier certificates that can be assembled into an augmented control barrier certificate for the full network under small-gain conditions. This certificate then supplies a computable lower bound on the probability that the interconnected system remains safe. The key payoff is that the sum-of-squares optimization needed for the certificates depends only on the size of each subsystem rather than the total number of subsystems in the network.

Core claim

The authors present a compositional scheme that first augments each stochastic hybrid subsystem to unify continuous evolution and jumps, then defines augmented control sub-barrier certificates whose combination under small-gain compositional conditions yields an augmented control barrier certificate for the interconnected network, from which a guaranteed lower bound on the safety probability follows.

What carries the argument

Augmented control barrier certificates (A-CBC) constructed from augmented control sub-barrier certificates (A-CSBCs) via small-gain compositional conditions.

If this is right

Safety probability lower bounds hold for the entire interconnected network once the A-CBC is obtained.
Controller synthesis via sum-of-squares optimization scales with subsystem dimension rather than total network size.
The method applies directly to networks of 1000 nonlinear stochastic hybrid subsystems under varying interconnection topologies.
Both continuous flows and discrete jumps are handled uniformly inside the same augmented certificate framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same compositional structure could be tested on reachability or invariance problems beyond safety.
Tighter small-gain functions might reduce conservatism in the resulting probability bounds.
Subsystem-level SOS programs could be parallelized across many processors for even larger networks.

Load-bearing premise

The small-gain compositional conditions are satisfied so that augmented control sub-barrier certificates from individual subsystems can be combined into one for the full network.

What would settle it

A concrete network of stochastic hybrid subsystems satisfying the small-gain conditions for which the derived safety probability lower bound is violated in simulation.

Figures

Figures reproduced from arXiv: 2409.10018 by Abolfazl Lavaei, Behrad Samari, Mahdieh Zaker, Omid Akbarzadeh.

**Figure 1.** Figure 1: A control barrier certificate for stochastic dynamical systems. The initial level set of CBC is denoted by dashed line (i.e., B(x) = µ). a lower dimension (a.k.a., infinite abstractions) or with discrete-state sets (a.k.a., finite abstractions) [JP09, APLS08]. On the downside, the existing abstraction-based techniques rely on discretizing state/input sets and are not applicable to real-world high-dimension… view at source ↗

**Figure 2.** Figure 2: Interconnection of two SHS Φ1, Φ2. Definition 2.3. Consider an SHS Φi = (Xi , Ui , Ui , Wi , Wi , σi , ρi , f1i , ςi , f2i ) with jump parameters (τ , ε1i , ε2i ). An augmented SHS (A-SHS) Ai(Φi) associated to Φi is characterized by Ai(Φi)= (Xi , Ui ,Wi , σi , ρi , ςi , Fi , Yi , Hi), where: • Xi = Xi × {0, . . . , ε2i } is the state space of A-SHS, while (xi , ϑi) ∈ Xi indicates that the current state is … view at source ↗

**Figure 3.** Figure 3: Control barrier certificate of a representative subsystem within the interconnected SHS Φ for a1 = −0.4, b1 = 0.5, a2 = 0.01, b2 = 0.06 (left), a1 = −0.3, b1 = 0.2, a2 = 1.01, b2 = 1 (middle), a1 = 0.01, b1 = 0.7, a2 = 0.02, b2 = 0.9 (right). Initial and unsafe regions are depicted by green and red boxes. Moreover, B¯ i(xi) = ¯µi and B¯ i(xi) = β¯ i indicated by and , respectively. that imply the satisfac… view at source ↗

**Figure 4.** Figure 4: Closed-loop state trajectories of a representative subsystem within the interconnected SHS Φ with 10 noise realizations for a1 = −0.4, b1 = 0.5, a2 = 0.01, b2 = 0.06 (left), a1 = −0.3, b1 = 0.2, a2 = 1.01, b2 = 1 (middle), a1 = 0.01, b1 = 0.7, a2 = 0.02, b2 = 0.9 (right). of the interconnected SHS Φ for different bounds with 10 noise realizations are depicted in [PITH_FULL_IMAGE:figures/full_fig_p021_4.png] view at source ↗

read the original abstract

In this work, we propose a compositional scheme based on small-gain reasoning to synthesize safety controllers for interconnected stochastic hybrid systems. In our proposed setting, we first offer an augmented scheme that characterizes each stochastic hybrid subsystem, endowed with both continuous evolution and instantaneous jumps, within a unified framework including both scenarios, implying that its state trajectories coincide with those of the original hybrid subsystem. We then introduce the concept of augmented control sub-barrier certificates (A-CSBCs) for each subsystem, thereby enabling the construction of an augmented control barrier certificate (A-CBC) for an interconnected network (from A-CSBCs of its subsystems) along with its safety controller under small-gain compositional conditions. We eventually leverage the constructed A-CBC to derive a guaranteed lower bound on the safety probability of the interconnected network. While in a monolithic scheme the computational complexity of synthesizing a control barrier certificate via sum-of-squares (SOS) optimization scales polynomially with the overall network size, the proposed compositional framework reduces this dependence to the subsystem size. We illustrate the efficacy of the proposed approach on an interconnected network comprising 1000 stochastic hybrid subsystems with nonlinear dynamics under two distinct interconnection topologies.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper introduces A-CSBCs and A-CBCs for compositional safety synthesis in stochastic hybrid systems and shows an example on 1000 subsystems, but the small-gain conditions are the part that must be checked to confirm the claimed complexity reduction.

read the letter

The key takeaway from this paper is a compositional safety controller synthesis for large stochastic hybrid systems using new augmented control sub-barrier certificates that combine continuous and jump dynamics. It claims to deliver a lower bound on safety probability while cutting computational complexity from scaling with the full network to just the subsystem size, illustrated on 1000 subsystems. The new elements are the A-CSBC and A-CBC definitions that allow small-gain composition in this hybrid stochastic setting. The paper handles the unification of dynamics well and applies the method to nonlinear cases with two interconnection topologies, which shows they have worked through a substantial example. A potential soft spot is the small-gain conditions themselves. The complexity reduction depends on these conditions being checkable without a cost that grows with the number of subsystems. The abstract does not explain how they are satisfied or verified in the 1000-subsystem case, so it is not clear if the claimed reduction holds in practice or if some global step remains. If the paper includes explicit checks or local conditions that stay small, that would strengthen it. This work is for control engineers and theorists interested in scalable safety verification for interconnected systems. Readers who follow barrier certificate methods or small-gain theorems will see the extension clearly. It deserves a serious referee because the scalability issue is important and the formal approach is laid out, even with the need for more detail on the conditions. Recommendation: Send it to peer review so the community can examine the example and the condition verification closely.

Referee Report

2 major / 1 minor

Summary. The paper proposes a compositional scheme based on small-gain reasoning to synthesize safety controllers for large-scale interconnected stochastic hybrid systems. It defines an augmented scheme that unifies continuous evolution and jumps for each subsystem, introduces augmented control sub-barrier certificates (A-CSBCs) per subsystem, and shows how these combine into an augmented control barrier certificate (A-CBC) for the network under small-gain conditions, yielding a lower bound on the network safety probability. The key claim is that this reduces SOS-based synthesis complexity from polynomial in network size to depending only on subsystem size, illustrated on a network of 1000 nonlinear stochastic hybrid subsystems under two interconnection topologies.

Significance. If the small-gain conditions can be verified without requiring a joint program whose size grows with the number of subsystems, the result would offer a practical route to scalable safety controller synthesis for large stochastic hybrid systems, extending prior small-gain and SOS barrier-certificate techniques while preserving formal probabilistic guarantees.

major comments (2)

[Abstract] Abstract (paragraph on small-gain compositional conditions): the central complexity-reduction claim requires that the small-gain conditions be satisfiable and verifiable with effort independent of network size; the manuscript provides no indication of how these conditions (e.g., any matrix inequality or joint SOS program) are checked or satisfied for either of the two 1000-subsystem topologies, which directly undermines the asserted polynomial-to-subsystem scaling.
[Abstract] Abstract (paragraph on augmented scheme): the claim that the augmented subsystem trajectories coincide with those of the original hybrid system is used to justify the A-CSBC construction, yet no proof outline or reference to the relevant theorem establishing this equivalence is supplied, leaving the preservation of safety properties unverified in the provided description.

minor comments (1)

The abstract refers to 'two distinct interconnection topologies' without naming them or indicating whether the small-gain matrix changes with topology.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for the opportunity to respond to the referee's report. We address each major comment below, providing clarifications from the manuscript and indicating revisions to the abstract where the presentation can be improved.

read point-by-point responses

Referee: [Abstract] Abstract (paragraph on small-gain compositional conditions): the central complexity-reduction claim requires that the small-gain conditions be satisfiable and verifiable with effort independent of network size; the manuscript provides no indication of how these conditions (e.g., any matrix inequality or joint SOS program) are checked or satisfied for either of the two 1000-subsystem topologies, which directly undermines the asserted polynomial-to-subsystem scaling.

Authors: We thank the referee for this observation. The small-gain conditions in our framework are expressed as a set of inequalities involving the individual subsystem gains (see Theorem 3.5), which are verified separately for each subsystem without requiring a joint optimization whose size grows with the network. In the examples of Section 5, the parameters are chosen such that these inequalities hold by design for both topologies. To address the lack of indication in the abstract, we will revise it to note that the conditions are satisfied via per-subsystem gain inequalities independent of network size. revision: yes
Referee: [Abstract] Abstract (paragraph on augmented scheme): the claim that the augmented subsystem trajectories coincide with those of the original hybrid system is used to justify the A-CSBC construction, yet no proof outline or reference to the relevant theorem establishing this equivalence is supplied, leaving the preservation of safety properties unverified in the provided description.

Authors: The equivalence is formally established in Proposition 2.3, which proves that the augmented scheme unifies continuous evolution and jumps while preserving the original state trajectories. This is used in the definition of A-CSBCs in Section 3. We agree that the abstract would benefit from referencing this result to clarify the justification. We will update the abstract accordingly in the revised version. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation relies on external small-gain theorems and standard SOS techniques

full rationale

The paper defines augmented control sub-barrier certificates (A-CSBCs) for subsystems and constructs the network-level A-CBC under small-gain conditions drawn from established control-theory literature. The safety-probability bound and complexity reduction to subsystem size follow directly from these independent definitions and the compositional construction; no equation reduces to a fitted parameter renamed as a prediction, no self-citation supplies a load-bearing uniqueness theorem, and the small-gain conditions are not shown to be justified solely by the authors' prior work. The framework is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claim rests on standard small-gain composition theorems and the computational assumption that SOS programs can synthesize the required certificates at subsystem scale; new certificate objects are introduced without independent external evidence.

axioms (2)

domain assumption Small-gain theorem applies to the interconnection of stochastic hybrid subsystems under the stated conditions
Invoked to guarantee that local A-CSBCs compose into a global A-CBC (abstract section on small-gain compositional conditions).
domain assumption Sum-of-squares optimization can find the required polynomial certificates for each subsystem
Used for computational synthesis of A-CSBCs (abstract paragraph on SOS optimization).

invented entities (2)

Augmented control sub-barrier certificate (A-CSBC) no independent evidence
purpose: Characterizes safety for each stochastic hybrid subsystem including both continuous evolution and jumps in a unified framework
New object introduced to enable the compositional construction; no external falsifiable evidence provided beyond the paper's definition.
Augmented control barrier certificate (A-CBC) no independent evidence
purpose: Serves as the global certificate for the interconnected network derived from subsystem A-CSBCs
Constructed object whose existence depends on the small-gain conditions; introduced in this work.

pith-pipeline@v0.9.0 · 5747 in / 1660 out tokens · 30894 ms · 2026-05-23T21:11:49.695687+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

if ξ⊤(−Θ + Ψ) < 0 and ∑ ξi βi > ∑ ξi μi then B = ∑ ξi Bi is an A-CBC (Theorem 4.2)
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

small-gain compositional conditions allow A-CSBCs of subsystems to be combined into A-CBC

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

A Physics-Informed Scenario Approach with Data Mitigation for Safety Verification of Nonlinear Systems
eess.SY 2024-12 unverdicted novelty 5.0

A physics-informed scenario approach selects data samples close to a physics model to reduce dataset size while constructing guaranteed barrier certificates for infinite-horizon safety of nonlinear systems.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages · cited by 1 Pith paper

[1]

A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada. Control barrier functions: Theory and applications. In Proceedings of the 18th European Control Conference (ECC) , pages 3420--3431, 2019

work page 2019
[2]

Anand, A

M. Anand, A. Lavaei, and M. Zamani. From small-gain theory to compositional construction of barrier certificates for large-scale stochastic systems. IEEE Transactions on Automatic Control , 67(10):5638--5645, 2022

work page 2022
[3]

Abate, M

A. Abate, M. Prandini, J. Lygeros, and S. Sastry. Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems. Automatica , 44(11):2724--2734, 2008

work page 2008
[4]

Ahmadi, A

M. Ahmadi, A. Singletary, J. W. Burdick, and A. D. Ames. Safe policy synthesis in multi-agent POMDPs via discrete-time barrier functions. In Proceedings of the 58th Conference on Decision and Control (CDC) , pages 4797--4803, 2019

work page 2019
[5]

Baier and J.-P

C. Baier and J.-P. Katoen. Principles of model checking . MIT press, 2008

work page 2008
[6]

H. AP. Blom, J. Lygeros, M. Everdij, S. Loizou, and K. Kyriakopoulos. Stochastic hybrid systems: theory and safety critical applications , volume 337. Springer, 2006

work page 2006
[7]

Borrmann, L

U. Borrmann, L. Wang, A. D. Ames, and M. Egerstedt. Control barrier certificates for safe swarm behavior. IFAC-PapersOnLine , 48(27):68--73, 2015

work page 2015
[8]

C. G. Cassandras and J. Lygeros. Stochastic hybrid systems . CRC Press, 2006

work page 2006
[9]

A. Clark. Control barrier functions for complete and incomplete information stochastic systems. In Proceedings of the American Control Conference (ACC) , pages 2928--2935, 2019

work page 2019
[10]

E. B. Dynkin. M arkov processes. pages 77--104. Springer, 1965

work page 1965
[11]

T. H. Gronwall. Note on the derivatives with respect to a parameter of the solutions of a system of differential equations. Annals of Mathematics , pages 292--296, 1919

work page 1919
[12]

E. M. Hahn, A. Hartmanns, H. Hermanns, and J.-P. Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design , 43(2):191--232, 2013

work page 2013
[13]

Jahanshahi, A

N. Jahanshahi, A. Lavaei, and M. Zamani. Compositional construction of safety controllers for networks of continuous-space POMDPs . IEEE Transactions on Control of Network Systems , 10(1):87--99, 2022

work page 2022
[14]

A. A. Julius and G. J. Pappas. Approximations of stochastic hybrid systems. IEEE Transactions on Automatic Control , 54(6):1193--1203, 2009

work page 2009
[15]

H. J. Kushner. Stochastic Stability and Control . Mathematics in Science and Engineering. Elsevier Science, 1967

work page 1967
[16]

A. Lavaei. Abstraction-based synthesis of stochastic hybrid systems. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages 1--11, 2024

work page 2024
[17]

Lavaei and E

A. Lavaei and E. Frazzoli. Scalable synthesis of safety barrier certificates for networks of stochastic switched systems. IEEE Transactions on Automatic Control , 2024

work page 2024
[18]

Lavaei, S

A. Lavaei, S. Soudjani, A. Abate, and M. Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica , 146, 2022

work page 2022
[19]

Lavaei, S

A. Lavaei, S. Soudjani, and E. Frazzoli. Safety barrier certificates for stochastic hybrid systems. In American Control Conference (ACC) , pages 880--885, 2022

work page 2022
[20]

Lavaei and M

A. Lavaei and M. Zamani. From dissipativity theory to compositional synthesis of large-scale stochastic switched systems. IEEE Transactions on Automatic Control , 67(9):4422--4437, 2022

work page 2022
[21]

Nejati, S

A. Nejati, S. Prakash Nayak, and A.-K. Schmuck. Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages 1--12, 2024

work page 2024
[22]

Nejati and M

A. Nejati and M. Zamani. Compositional construction of finite MDPs for continuous-time stochastic systems: A dissipativity approach. IFAC-PapersOnLine , 53(2):1962--1967, 2020

work page 1962
[23]

Nejati and M

A. Nejati and M. Zamani. From dissipativity theory to compositional construction of control barrier certificates. Leibniz Transactions on Embedded Systems (LITES) (Special Issue on Distributed Hybrid Systems) , 8(2), 2022

work page 2022
[24]

Oksendal

B. Oksendal. Stochastic differential equations: an introduction with applications . Springer Science & Business Media, 2013

work page 2013
[25]

B. K. ksendal and A. Sulem. Applied stochastic control of jump diffusions , volume 498. Springer, 2005

work page 2005
[26]

P. A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical programming , 96(2):293--320, 2003

work page 2003
[27]

Papachristodoulou, J

A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo. SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB . arXiv:1310.4716 , 2013

work page arXiv 2013
[28]

Prajna and A

S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control (HSCC) , pages 477--492, 2004

work page 2004
[29]

Prajna, A

S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control , 52(8):1415--1428, 2007

work page 2007
[30]

Santoyo, M

C. Santoyo, M. Dutreix, and S.l Coogan. Verification and control for finite-time safety of stochastic systems via barrier functions. In Proceedings of the IEEE Conference on Control Technology and Applications , pages 712--717, 2019

work page 2019
[31]

J. F. Sturm. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization methods and software , 11(1-4):625--653, 1999

work page 1999
[32]

PRoTECT : Parallelized construction of safety barrier certificates for nonlinear polynomial systems

Ben Wooding, Viacheslav Horbanov, and Abolfazl Lavaei. PRoTECT : Parallelized construction of safety barrier certificates for nonlinear polynomial systems. arXiv:2404.14804 , 2024

work page arXiv 2024
[33]

Wongpiromsarn, U

T. Wongpiromsarn, U. Topcu, and A. Lamperski. Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Transactions on Automatic Control , 61(11):3344--3355, 2015

work page 2015
[34]

Zhang, L.and She, S

Z. Zhang, L.and She, S. Ratschan, H. Hermanns, and E. M. Hahn. Safety verification for probabilistic hybrid systems. In CAV , pages 196--211, 2010

work page 2010
[35]

write newline

" write newline "" initialize.prev.this.status FUNCTION begin.bib " write newline preamble empty 'skip preamble write newline if " thebibliography " longest.label * " " * write newline " [1] #1 " write newline " url@samestyle " write newline " " write newline " [2] #2 " write newline " =0pt " write newline " " ALTinterwordstretchfactor * " " * write newli...

work page

[1] [1]

A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada. Control barrier functions: Theory and applications. In Proceedings of the 18th European Control Conference (ECC) , pages 3420--3431, 2019

work page 2019

[2] [2]

Anand, A

M. Anand, A. Lavaei, and M. Zamani. From small-gain theory to compositional construction of barrier certificates for large-scale stochastic systems. IEEE Transactions on Automatic Control , 67(10):5638--5645, 2022

work page 2022

[3] [3]

Abate, M

A. Abate, M. Prandini, J. Lygeros, and S. Sastry. Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems. Automatica , 44(11):2724--2734, 2008

work page 2008

[4] [4]

Ahmadi, A

M. Ahmadi, A. Singletary, J. W. Burdick, and A. D. Ames. Safe policy synthesis in multi-agent POMDPs via discrete-time barrier functions. In Proceedings of the 58th Conference on Decision and Control (CDC) , pages 4797--4803, 2019

work page 2019

[5] [5]

Baier and J.-P

C. Baier and J.-P. Katoen. Principles of model checking . MIT press, 2008

work page 2008

[6] [6]

H. AP. Blom, J. Lygeros, M. Everdij, S. Loizou, and K. Kyriakopoulos. Stochastic hybrid systems: theory and safety critical applications , volume 337. Springer, 2006

work page 2006

[7] [7]

Borrmann, L

U. Borrmann, L. Wang, A. D. Ames, and M. Egerstedt. Control barrier certificates for safe swarm behavior. IFAC-PapersOnLine , 48(27):68--73, 2015

work page 2015

[8] [8]

C. G. Cassandras and J. Lygeros. Stochastic hybrid systems . CRC Press, 2006

work page 2006

[9] [9]

A. Clark. Control barrier functions for complete and incomplete information stochastic systems. In Proceedings of the American Control Conference (ACC) , pages 2928--2935, 2019

work page 2019

[10] [10]

E. B. Dynkin. M arkov processes. pages 77--104. Springer, 1965

work page 1965

[11] [11]

T. H. Gronwall. Note on the derivatives with respect to a parameter of the solutions of a system of differential equations. Annals of Mathematics , pages 292--296, 1919

work page 1919

[12] [12]

E. M. Hahn, A. Hartmanns, H. Hermanns, and J.-P. Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design , 43(2):191--232, 2013

work page 2013

[13] [13]

Jahanshahi, A

N. Jahanshahi, A. Lavaei, and M. Zamani. Compositional construction of safety controllers for networks of continuous-space POMDPs . IEEE Transactions on Control of Network Systems , 10(1):87--99, 2022

work page 2022

[14] [14]

A. A. Julius and G. J. Pappas. Approximations of stochastic hybrid systems. IEEE Transactions on Automatic Control , 54(6):1193--1203, 2009

work page 2009

[15] [15]

H. J. Kushner. Stochastic Stability and Control . Mathematics in Science and Engineering. Elsevier Science, 1967

work page 1967

[16] [16]

A. Lavaei. Abstraction-based synthesis of stochastic hybrid systems. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages 1--11, 2024

work page 2024

[17] [17]

Lavaei and E

A. Lavaei and E. Frazzoli. Scalable synthesis of safety barrier certificates for networks of stochastic switched systems. IEEE Transactions on Automatic Control , 2024

work page 2024

[18] [18]

Lavaei, S

A. Lavaei, S. Soudjani, A. Abate, and M. Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica , 146, 2022

work page 2022

[19] [19]

Lavaei, S

A. Lavaei, S. Soudjani, and E. Frazzoli. Safety barrier certificates for stochastic hybrid systems. In American Control Conference (ACC) , pages 880--885, 2022

work page 2022

[20] [20]

Lavaei and M

A. Lavaei and M. Zamani. From dissipativity theory to compositional synthesis of large-scale stochastic switched systems. IEEE Transactions on Automatic Control , 67(9):4422--4437, 2022

work page 2022

[21] [21]

Nejati, S

A. Nejati, S. Prakash Nayak, and A.-K. Schmuck. Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control , pages 1--12, 2024

work page 2024

[22] [22]

Nejati and M

A. Nejati and M. Zamani. Compositional construction of finite MDPs for continuous-time stochastic systems: A dissipativity approach. IFAC-PapersOnLine , 53(2):1962--1967, 2020

work page 1962

[23] [23]

Nejati and M

A. Nejati and M. Zamani. From dissipativity theory to compositional construction of control barrier certificates. Leibniz Transactions on Embedded Systems (LITES) (Special Issue on Distributed Hybrid Systems) , 8(2), 2022

work page 2022

[24] [24]

Oksendal

B. Oksendal. Stochastic differential equations: an introduction with applications . Springer Science & Business Media, 2013

work page 2013

[25] [25]

B. K. ksendal and A. Sulem. Applied stochastic control of jump diffusions , volume 498. Springer, 2005

work page 2005

[26] [26]

P. A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical programming , 96(2):293--320, 2003

work page 2003

[27] [27]

Papachristodoulou, J

A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo. SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB . arXiv:1310.4716 , 2013

work page arXiv 2013

[28] [28]

Prajna and A

S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control (HSCC) , pages 477--492, 2004

work page 2004

[29] [29]

Prajna, A

S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control , 52(8):1415--1428, 2007

work page 2007

[30] [30]

Santoyo, M

C. Santoyo, M. Dutreix, and S.l Coogan. Verification and control for finite-time safety of stochastic systems via barrier functions. In Proceedings of the IEEE Conference on Control Technology and Applications , pages 712--717, 2019

work page 2019

[31] [31]

J. F. Sturm. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization methods and software , 11(1-4):625--653, 1999

work page 1999

[32] [32]

PRoTECT : Parallelized construction of safety barrier certificates for nonlinear polynomial systems

Ben Wooding, Viacheslav Horbanov, and Abolfazl Lavaei. PRoTECT : Parallelized construction of safety barrier certificates for nonlinear polynomial systems. arXiv:2404.14804 , 2024

work page arXiv 2024

[33] [33]

Wongpiromsarn, U

T. Wongpiromsarn, U. Topcu, and A. Lamperski. Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Transactions on Automatic Control , 61(11):3344--3355, 2015

work page 2015

[34] [34]

Zhang, L.and She, S

Z. Zhang, L.and She, S. Ratschan, H. Hermanns, and E. M. Hahn. Safety verification for probabilistic hybrid systems. In CAV , pages 196--211, 2010

work page 2010

[35] [35]

write newline

" write newline "" initialize.prev.this.status FUNCTION begin.bib " write newline preamble empty 'skip preamble write newline if " thebibliography " longest.label * " " * write newline " [1] #1 " write newline " url@samestyle " write newline " " write newline " [2] #2 " write newline " =0pt " write newline " " ALTinterwordstretchfactor * " " * write newli...

work page