Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey

1. Introduction

• The survey focuses on formal verification and policy synthesis for stochastic hybrid systems, where interacting discrete and continuous dynamics and uncertainty complicate analysis.Verification checks specification satisfaction; synthesis designs a controller to enforce or optimize satisfaction probability.Source: §1 · pp. 1–2

1.1. Discretization-based Techniques.

• Finite abstractions approximate concrete systems with finite-state models, enabling analysis and controller synthesis whose guarantees can be refined back to the original system.The discrete controller may be a static lookup table or a dynamic controller with finite memory.Source: §1.1 · p. 2, Figure 1 · p. 3

1.2. Discretization-free Techniques.

• Finite-state gridding faces exponentially growing construction complexity with state and input dimension; barrier certificates offer a discretization-free safety route, while time-domain model reduction addresses trajectory properties.Barrier certificates use Lyapunov-like functions and suitable level sets to separate unsafe regions from trajectories starting in a given set with a probability lower bound.Source: §1.2 · pp. 2–4

1.3. Different Types of Closeness Guarantees.

• The survey distinguishes four abstraction-closeness guarantees: satisfaction-probability differences, probabilistic and expected output-trajectory differences, and probability bounds transferred between abstract and concrete models.Specification-guided abstractions may be less conservative, while specification-free abstractions cover broader property classes at greater computational cost.Source: §1.3 · p. 4

1.4. Contributions and Organization of this Survey.

• As the first survey focused on automated formal verification and synthesis of stochastic hybrid systems, it reviews recent approaches, algorithms, complexity and memory considerations, software tools, and open research problems.Coverage includes finite and infinite abstractions, barrier certificates, temporal logic, compositional methods, and selected continuous-time results.Source: §1.4 · pp. 4–5

2. Notations, Preliminaries, and Models

• The notation section fixes conventions for sets, vectors, norms, matrices, relations, probability spaces, and measurable maps.It defines Borel spaces and assumes random variables are measurable, inducing probability measures on their state spaces.Source: §2 · pp. 5–6

2.1. Discrete-Time Stochastic Hybrid Systems.

• A dt-SHS is modeled with hybrid states, inputs, a stochastic transition kernel, and outputs; the survey focuses on single-mode dt-SCS, equivalently represented by a state-update function and i.i.d. noise.The dt-SCS representation is used for easier presentation, with the stated notions and approaches generalizable to hybrid state spaces.Source: §2.1 · pp. 6–7

2.2. Relations between Models.

• δ-ISS bounds differences between solution processes, while an SSF relates concrete and abstract output trajectories and supports transferring analysis from an abstraction to the original system.An SSF also yields an interface function for refining an abstract synthesized policy into a concrete-system policy.Source: §2.2 · p. 9

2.3. Temporal Logic Specifications.

• Safety, reachability, and reach-avoid requirements are expressed over output trajectories with bounded- or infinite-horizon temporal properties, including LTL specifications.LTL likelihoods require reasoning about measurability of specification events, which the survey does not address in depth.Source: §2.3 · pp. 9–10
• scLTL properties, whose satisfaction can be witnessed by finite traces, can be represented by finite-state automata; the survey considers bounded-horizon probabilities of accepting words.An scLTL formula has an equivalent DFA, enabling computation of the probability that a word of length at most Td + 1 is accepted.Source: §2.3 · pp. 10–11
• An infinite word satisfies an ω-regular property when an accepting automaton run exists; nondeterministic Büchi automata capture LTL and require nondeterminism for this expressiveness.Acceptance requires visiting accepting locations infinitely often.Source: §2.3 · pp. 11–12
• LTL satisfaction is defined over trajectories, whereas PCTL adds probabilistic operators and defines satisfaction over states using branching semantics.PCTL probability is taken over the infinite paths induced by the stochastic dynamics.Source: §2.3 · p. 12
• Prior work characterizes PCTL safety, reachability, invariance, and reach-avoid properties for dt-SCS using dynamic-programming recursions.Further work generalizes the characterization to regular and ω-regular properties using DFA and deterministic NBA models.Source: §2.3 · pp. 12–13
• The survey assumes its random variables and specifications are measurable, allowing probabilities to be assigned to specification events under system dynamics [Var85, Proposition 2.3].Source: §2.3 · p. 13
• The survey focuses on safety, reachability, reach-avoid, LTL, and PCTL, while noting that SHS literature also uses scLTL, BLTL, STL, and MITL.These are presented as simpler, common requirements used in both literature and practice.Source: §2.3 · p. 13

3. Stochastic Similarity Relations for Abstractions

• Four theorems summarize distinct closeness guarantees between concrete SHS models and abstractions, including satisfaction-probability bounds and output-trajectory guarantees.The first discrete-time result bounds the difference in satisfaction probabilities under a Lipschitz-continuity assumption on the stochastic kernel.Source: §3 · pp. 13–14
• The error formulas involving the state-space Lebesgue measure are meaningful on bounded domains and can be conservative; adaptive sequential gridding may mitigate both issues.The abstraction may also depend on the specification being interpreted on the abstract model.Source: §3 · p. 14
• Satisfaction-probability bounds based on stochastic-kernel Lipschitz constants depend on the specification, while a trajectory-based bound is specification-free but likely more complex to compute and less tight.The trajectory guarantee requires incremental input-to-state stability; the satisfaction-probability bound instead requires Lipschitz continuity of the stochastic kernel.Source: §3 · p. 15
• When noise standard deviation approaches zero, the Lipschitz-based abstraction error grows without bound, whereas the trajectory bound does not; the latter can outperform it if the model is δ-ISS.The δ-lifting approach uses ε-expansions or ε-contractions of the abstract system’s event sets to bound concrete satisfaction probabilities.Source: §3 · p. 15
• For measurable events, probabilities over ε-expanded and ε-contracted abstract sets provide upper and lower bounds on concrete satisfaction probabilities, with quantified error bounds.The construction applies to temporal-logic properties accepted by a deterministic finite automaton.Source: §3 · p. 16

3.1. Literature on Similarity Relations for Stochastic Models.

• A lifted approximate relation trades deviations between state distributions against metric distances between outputs and supports verification and synthesis for discrete-time stochastic control systems.An interface function refines an abstract policy for the concrete system.Source: §3.1 · p. 17
• Later work extends these relations to bounded probabilistic reachability and co-safe LTL, robust policy synthesis, and networks of discrete-time stochastic control systems.An open problem is computing a probabilistic bisimilarity distance between two such systems for any ω-regular specification.Source: §3.1 · pp. 17–18

4. Infinite Abstractions

• Infinite abstractions use simpler dynamics or lower-dimensional state spaces to reduce system complexity before analysis and synthesis, with results refined back through an interface map.They can also precede finite abstractions, which may otherwise require impractically large state spaces for high-dimensional systems.Source: §4 · p. 18
• Stochastic simulation functions relate abstract and original output trajectories, bounding their mismatch and quantifying their probabilistic distance.The survey focuses on lower-dimensional infinite abstractions as compact representations of concrete models.Source: §4 · pp. 18–19
• For linear dt-SCS with independent additive noises, the theorem's matrix conditions yield a quadratic stochastic simulation function between the original and reduced models.The reduced state dimension is encoded by the column dimension of transformation matrix P.Source: §4 · pp. 19–20
• The stochastic simulation function gives a probabilistic closeness guarantee between the original system and its infinite abstraction.The guarantee bounds the probabilistic distance between their output trajectories.Source: §4 · p. 20
• The abstract input matrix ˆB can be chosen arbitrarily, including as an identity matrix for full actuation; choosing ˆR=0 tightens the bound except when both systems share noise.In the shared-noise setting, ˆR can instead be selected to minimize the error term.Source: §4 · p. 20
• [LSZ19] also constructs infinite abstractions using stochastic storage functions for a class of nonlinear stochastic systems with slope-restricted nonlinearities.The storage function provides a closeness guarantee, and the work proposes a construction scheme for abstractions and their corresponding functions.Source: §4 · p. 20
• The approaches in allow independent concrete and abstract noises, unlike, which assumes the abstraction shares the concrete system's noise.Both approaches provide probabilistic closeness guarantees between output trajectories.Source: §4 · p. 20
• ε=1 over Td=100 with probability at least 95% for the two-room example, using ˆR=0.01 and equal initial states of 20.The example constructs a one-dimensional infinite abstraction of a two-dimensional room-temperature model.Source: §4 · p. 21

5. Finite Abstractions

• Finite MDP abstractions partition compact state and input sets, select representative points, and support automated synthesis of controllers that can be refined over the concrete model.Compactness can be relaxed at the cost of additional quantifiable approximation error, and refining state partitions reduces error without requiring a particular partition shape.Source: §5 · pp. 21–22

5.1. Abstractions for Finite-Horizon Specifications.

• Finite-horizon methods use adaptive gridding and probabilistic closeness bounds, while some approaches handle discontinuous kernels or exploit higher derivatives for faster error convergence.The framework does not require δ-ISS, but its error depends on kernel Lipschitz constants and grows unbounded as noise standard deviation approaches zero; the cited methods avoid that behavior.Source: §5.1 · p. 23
• With δ = 0.005, outputs remain within ε = 0.5 over Td = 100 with probability at least 98%; 10,000 simulations also matched a 0.1-distance bound at 98%.The authors attribute the tighter empirical outcomes to conservatism in simulation-function bounds.Source: §5.1 · p. 25

5.2. Abstractions for Infinite-Horizon Specifications.

• For continuous-state dt-SCS with a compact safe set, infinite-horizon safety probability is zero everywhere if and only if the safe set contains no absorbing set.Finite MDP absorbing sets can be found as bottom strongly connected components, but the survey identifies computing or approximating absorbing sets for continuous-state systems as an open problem.Source: §5.2 · p. 27

5.3. Abstractions as Interval Markov Models.

• Interval Markov abstractions bound transition probabilities above and below; mixed monotonicity with independent unimodal noise can avoid the required max-min optimization.Related methods verify omega-regular properties on interval chains and extend to controller synthesis for switched systems using bounded-parameter MDPs.Source: §5.3 · pp. 27–28
• Because [DC19] and [DHC20] assume additive stochasticity, unimodal noise, and independence across states, defining stochastic-kernel mixed monotonicity and identifying systems satisfying it remains open.The paper points to an initial investigation in Subsection 12.4.Source: §5.3 · p. 28
• [LAB15] maps discrete-time stochastic systems to IMCs and switched systems to BMDPs for PCTL classification, satisfaction-maximizing policy synthesis, and adaptive refinement.The framework also provides a closeness guarantee.Source: §5.3 · p. 28
• [ZLWDA18] interval-MDP abstractions have smaller one-step bisimulation error than Markov-chain abstractions, with computational complexity comparable to standard approximate-bisimulation methods.The work also outlines probabilistic model checking.Source: §5.3 · pp. 28–29
• [ADB11] gives a constructive finite abstraction of discrete-time SHS usable over infinite horizons, with errors explicitly computed and tunable through the state-space partition under continuity assumptions.The partition depends on a controllable parameter.Source: §5.3 · p. 29
• [CLL+19] embeds exactly computed convex-optimization abstraction errors in IMDPs for synthesis over bounded and unbounded temporal properties, mitigating state-space explosion but lacking convergence guarantees.The method treats discrete-time SHS with linear dynamics and maps a maximizing strategy back to the system.Source: §5.3 · p. 29
• [BAJ+22] uses scenario-based PAC assertions to build IMDPs robust to unknown disturbances, with interval tightness controlled by sample count and guarantees transferred to the concrete system.Verification on the IMDP yields a controller with probabilistic guarantees for safely reaching a target.Source: §5.3 · p. 29
• For IMC/IMDP approaches, quantifying the distance between satisfaction probabilities across abstract and original systems remains open, beyond the usual lower-bound guarantee.The existing guarantee gives a lower bound on the original system’s satisfaction probability.Source: §5.3 · p. 29

6. Discretization-Free Verification & Synthesis

• CBCs bound unsafe-reach probabilities over finite horizons, with infinite-horizon guarantees available when c = 0.The c = 0 condition makes B a non-negative supermartingale, though such a certificate may not exist; the more general c-martingale condition gives finite-horizon guarantees.Source: §6 · p. 30

6.1.1. Sum-of-Squares Optimization Problems

• Under polynomial dynamics and bounded semi-algebraic state and input sets, SOS optimization can find a polynomial CBC and controller.The SOS formulation uses sum-of-squares multipliers; SOSTOOLS and an SDP solver are cited as available tools.Source: §6.1.1 · p. 31

6.1.2. Counter-Example Guided Inductive Synthesis

• CEGIS searches for CBCs by iteratively adding SMT counterexamples to a finite sample set, and derives a policy from a finite input set.A candidate is certified when the negation of the verification condition is infeasible; the approach does not require dynamics restrictions beyond those of the chosen SMT solver.Source: §6.1.2 · pp. 31–32
• SOS complexity depends on polynomial degree and state dimension, while CEGIS depends on an iterative SMT search without termination guarantees.For fixed polynomial degree, SOS computation grows polynomially with dimension; finite-MDP construction grows exponentially with state dimension.Source: §6.1.2 · p. 32

6.1.3. Related Work on Barrier Certificates

• Barrier-certificate methods bound satisfaction probabilities for safe-LTL properties of stochastic systems and extend to synthesis; certificate existence is not guaranteed, and constructing CBCs for general nonlinear dt-SCS remains open.Source: §6.1.3 · pp. 32–33
• For the room-temperature example, the synthesized controller keeps the temperature in [17, 23] with probability at least 95% over Td = 10.The example starts from X0 = [19.5, 20]; the reported CBC and controller are polynomial functions of temperature.Source: §6.1.3 · p. 33

6.2. Analysis of SHS with Optimization-based Methods

• SMPC is challenging for nonlinear dynamics or non-convex constraints, and does not straightforwardly encode complex high-level logical properties.Recursive feasibility may ensure a form of invariance, but formal verification and synthesis guarantees for complex SHS remain an open challenge for SMPC.Source: §6.2 · p. 34

7. Temporal Logic Verification and Synthesis

• Abstraction-based synthesis translates specifications into automata, forms a product process, and discretizes the problem into finite MDP dynamic programs.The resulting policies are history-independent Markov policies, with quantified approximation errors; a generalization reduces broad LTL and ω-regular objectives to reachability or repeated reachability.Source: §7 · p. 35
• Similarity-based refinement uses an epsilon-perturbed specification to transfer satisfaction guarantees from abstract models to concrete systems.These approaches quantify probabilistic distance; the perturbed specification is represented by a modified DFA with an absorbing state.Source: §7 · p. 35
• Control barrier certificates support safe-LTL verification and synthesis over finite traces, with an extension to ω-regular specifications [ALZ21a].The safe-LTL approach decomposes the negated specification into sequential reachabilities and bounds their probabilities.Source: §7 · p. 35
• Other surveyed reachability methods include Fourier-transform analysis for linear systems, Lagrangian under-approximation, and game-based reach-avoid formulations.The Lagrangian approach can avoid gridding but remains conservative; its scalability depends on geometrical computations.Source: §7 · pp. 35–36
• Multi-objective approaches prioritize safety or encode specifications with different priorities, while robotic deployment work combines finite-state MDPs with probabilistic-logic specifications [LA18, HNS21, LAB11].The survey also points to a tutorial on trade-offs among quantitative properties.Source: §7 · p. 36
• For unknown continuous-space dt-SCS, model-free reinforcement learning synthesizes strategies that maximize scLTL satisfaction probability within a bounded time horizon and provides probabilistic closeness guarantees in the form of (3.3).Source: §7 · p. 37
• Approximate optimality guarantees for learning-based controllers satisfying arbitrary LTL specifications remain an open problem.The survey identifies this as a future research direction for dt-SCS.Source: §7 · p. 37

Compositional abstractions

• Local stochastic simulation functions yield an overall relation between an interconnected system and its abstraction when compositionality conditions hold.The conditions include sum-type or max-type small-gain approaches and dissipativity conditions.Source: §8 · pp. 39–40
• Sum-type small-gain methods require linear gain growth and give additive overall error, while max-type methods need no such linearity and use the maximum subsystem error.Checking the sum-type condition is easier because it uses a matrix spectral-radius test.Source: §8 · pp. 39–40
• A unified compositional scheme for approximate probabilistic relations is reported as less conservative than separately constructing infinite and finite abstractions.The scheme uses matrix conditions that incorporate network structure.Source: §8 · pp. 41–42

Open challenges

• Finite abstractions can still face the curse of dimensionality within individual subsystems, motivating compositional barrier-certificate construction.The survey also identifies compositional multi-objective synthesis for continuous-space SHS as an open problem for large-scale real-life applications.Source: §8 · p. 42

Barrier certificates

• Compositional barrier methods construct safety controllers for partially observed systems using local barriers and small-gain conditions.The schemes either need no prior estimation-accuracy knowledge or use a probability bound on that accuracy, and provide finite-horizon lower bounds on avoiding unsafe regions.Source: §8 · p. 42

Running example

• For two rooms, the same ε = 0.5 and Td = 100 output-distance bound holds with probability at least 98%.Ten simulated noise realizations satisfy the comfort-zone specification, consistent with the theoretical guarantee.Source: Figure 18 · p. 42, §8 · p. 43, Figure 19 · p. 43
• For 1,000 rooms, the proposed bound guarantees that the distance between outputs of Σ and bΣ stays at most ε = 0.5 over Td = 100 with probability at least 98%.Source: §8 · p. 44

Scope

• The survey selects continuous-time results across topics covered earlier in the paper, including symbolic models, barrier certificates, and temporal-logic methods.The section traces foundations to piecewise-deterministic Markov models and diffusion processes.Source: §9 · pp. 44–45

Stochastic similarity relations

• A stochastic simulation function and an interface can relate a continuous-time system to its abstraction for an input trajectory preserving the abstract closed-loop Markov property.The resulting theorem bounds the moment of the difference between their output trajectories.Source: §9 · p. 46
• The moment bound can support probability bounds for specifications checked at single time instances, such as reachability, but not general always or until properties.The latter require joint distributions across time instants, which the bound does not capture.Source: §9 · p. 46

Abstractions and verification

• For continuous-time SHS, prior work constructs abstractions for jump-linear systems and linear stochastic hybrid automata, and reduces other models to CTMCs for MITL verification.The CTMC approach partitions the state space and computes transition rates between partitions.Source: Infinite abstractions · p. 46

Symbolic models

• Symbolic models for incrementally stable stochastic control and switched systems provide approximately bisimilar finite abstractions, with one switched-system technique avoiding state-space discretization.The no-discretization technique may be more efficient for higher-dimensional switched systems.Source: Finite abstractions · pp. 46–47

Barrier certificates

• For polynomial-type systems, barrier certificates can use convex optimization to bound the probability of ever reaching an unsafe set over an infinite horizon.The approach relies on a supermartingale property.Source: Finite abstractions · p. 47
• Finite-time barrier methods allow state-dependent infinitesimal-generator bounds and can synthesize polynomial state-feedback controllers for affine-in-control drift dynamics.The controllers target a specified safety probability.Source: Finite abstractions · p. 47

Partial observation

• With partial state information, barrier-based synthesis can bound finite-horizon safety probability using an estimator with a probabilistic accuracy guarantee, without requiring stability or a supermartingale property.A generalized approach needs no prior estimation-accuracy knowledge and covers NFA properties and partially observed jump-diffusion systems.Source: Finite abstractions · p. 47

Compositional abstractions

• For jump-linear systems and linear stochastic hybrid automata, sum-type small-gain conditions support compositional infinite abstractions with quantified approximation error.The approach also gives a constructive scheme for approximations and their stochastic simulation functions.Source: Compositional techniques · p. 47
• Compositional finite abstractions are also reported for systems satisfying stochastic δ-ISS, and for continuous-time networks using timediscretized intermediate abstractions.The latter constructs finite MDPs and quantifies distance at sampling times.Source: Compositional techniques · pp. 47–48
• Compositional abstraction methods cover randomly switched interconnection topologies and dissipativity-based networks with stochastic noise and jumps.The surveyed methods provide moment-based closeness guarantees for these abstractions.Source: Compositional techniques · p. 48

Safety certificates

• Compositional pseudo-barrier functions support finite-horizon safety-controller synthesis for interconnected continuous-time systems.The method uses sum-type small-gain conditions and SOS optimization to search for subsystem certificates.Source: Compositional techniques · p. 48

Other methods and scope

• Other surveyed continuous-time approaches include reachability and safety analysis, temporal-logic control, and motion planning; the survey does not delve into stability analysis or optimal control.Its stability and optimal-control discussions are referred to other surveys and works.Source: Compositional techniques · pp. 48–49

Simulation-based analysis

• Early simulation work covers filtering for SHS, sequential Monte Carlo and Petri Nets for collision-risk estimation, air-traffic safety risk, and efficient Monte Carlo simulation.The proposed results also apply to rare-event estimation over complex models.Source: §10 · p. 50

Simulation-based guarantees

• Two-layer simulation-based guarantees use sampled data to assess a property at a threshold and confidence level, unlike the one-layer formal guarantees discussed earlier.Setting the confidence level to one makes the chance-constrained problem similar to the earlier formal guarantee.Source: §10 · p. 50

Statistical model checking

• An SMC algorithm verifies stochastic properties with unbounded until using Monte Carlo simulation and hypothesis testing of samples.For policy synthesis, another framework probabilistically resolves nondeterminism, then uses sampling and reinforcement learning to improve bounded linear temporal logic satisfaction.Source: §10 · p. 50
• A numerically rigorous Monte Carlo-SMT approach computes probabilistic-reachability confidence intervals for systems with random and nondeterministic parameters.It uses δ-complete SMT procedures and samples over-approximations of random quantities; the survey also notes a separate SMC survey on precision-scalability tradeoffs.Source: §10 · p. 50
• A multilevel Monte Carlo SMC method approximates continuous-time SHS with discrete-time processes that converge weakly for property satisfaction.For bounded-horizon reachability, it estimates an exit-time distribution through a discontinuous indicator functional, then smooths that functional and quantifies mean-square error from smoothing, bias, and variance.Source: §10 · pp. 50–51
• Sampling-based confidence intervals trade accuracy against computational effort while guaranteeing convergence to the exact solution.Other work applies Bayesian SMC to discrete-time Markov chains with continuous stochastic logic and integrates sequential Monte Carlo with approximate Bayesian inference.Source: §10 · p. 51

Research directions

• SMC approaches appear suitable for verification but less efficient for synthesis, which the survey identifies as an open problem.Most proposed SMC results suit finite horizons; infinite-horizon results require strong assumptions that are not generally satisfiable by SHS.Source: §10 · p. 51

11. Software Tools

• The software-tools survey focuses on tools available at the time of writing, relating their architectures to underlying theory and noting open-science initiatives.It frames software for verification, synthesis, and simulation as a growing area.Source: §11 · p. 51

11.1. The Modest Toolset.

• The Modest Toolset models networks of stochastic hybrid automata combining nondeterministic choices, continuous dynamics, stochastic decisions, timing, and real-time behavior.Its modular framework accepts the Modest language and provides analysis backends for special cases of these automata.Source: §11.1 · p. 51

11.2. SReach.

• SReach solves bounded-time reachability for nonlinear hybrid automata with parametric uncertainty and probabilistic hybrid automata with random transitions and resets.It combines δ-complete decision procedures and statistical tests, supporting nondeterministic branching and increased simulation coverage compared with standard simulation-based methods.Source: §11.2 · p. 51

11.3. ProbReach.

• ProbReach returns a numerically sound interval of at most ε containing the exact bounded-reachability probability for SHS with random continuous quantities and Lipschitz-continuous dynamics.It uses validated integration to partition the random quantities and enclose outcomes with under- and over-approximations; discrete-only random parameters do not retain the arbitrary-precision guarantee, while nondeterministic continuous parameters yield an enclosure that may exceed ε.Source: §11.3 · pp. 51–52

11. Software Tools

• SReachTools computes over- and under-approximations of stochastic reach sets for linear, potentially time-varying discrete-time systems with stochastic disturbances.It supports verification and open-loop or affine state-feedback controller synthesis for target-tube reachability and related problems.Source: §11.4 · p. 52

11.5. HYPEG.

• HYPEG statistically simulates hybrid Petri nets with general transitions, combining discrete and continuous components and arbitrary random-variable distributions.Its time-bounded discrete-event simulation and SMC techniques verify properties including bounded-time reachability.Source: §11.5 · p. 52

11.6. Mascot-SDS.

• Mascot-SDS synthesizes controllers with formal correctness guarantees for discrete-time dynamical systems under stochastic perturbations.Its current version supports “always eventually” specifications and approximates the states satisfying a specification with probability one.Source: §11.6 · p. 52
• The Level-Set Toolbox solves time-dependent Hamilton-Jacobi PDEs in Matlab and has been used to analyze stochastic models.Its source code is provided, and it is intended for experimentation alongside existing level-set literature.Source: §11.7 · p. 52

11.8. FAUST 2.

• FAUST2 generates formal abstractions of continuous-space discrete-time Markov processes and supports verification and synthesis for safety and reachability specifications.A user-defined maximum threshold controls abstraction error; users can export the abstract model to PRISM or Storm, or compute PCTL properties internally and refine outcomes over the concrete model.Source: §11.8 · pp. 52–53
• StocHy simulates discrete-time SHS and constructs finite abstractions for formal verification or control synthesis of safety and reachability specifications.Its independent simulation, verification, and synthesis libraries support modular modeling and extensions.Source: §11.9 · p. 53

11.10. AMYTISS.

• AMYTISS constructs finite MDPs and synthesizes controllers for complex logic properties on large-scale discrete-time stochastic control systems.It supports additive and multiplicative noise from several distributions and uses parallel execution across CPUs, GPUs, and hardware accelerators to improve computation time and memory usage.Source: §11.10 · p. 53
• AMYTISS reduces transition-matrix memory through a probability threshold γ and on-the-fly abstraction, which trades storage for repeated computation over the finite horizon.On-the-fly abstraction computes needed transition entries during synthesis instead of storing the matrix; the tool has been applied to large-scale applications including autonomous vehicles.Source: §11.10 · p. 53

11.11. The ARCH Initiative.

• The ARCH competition compares tools across models, platforms, algorithms, specifications, and stochasticity, using centralized benchmark execution and publicly released benchmark and results code.The benchmarks aim to provide a reference point and encourage tool development; the survey points readers to [ABC+20, Table 2] for recent outcomes.Source: §11.11 · p. 53

12.1. Formal Analysis of SHS via Learning and Data-Driven Approaches.

• Learning-based work covers policy gradients, temporal-logic objectives, and data-driven verification, but theoretical guarantees vary across settings.[S+14] provides no quantitative optimality guarantee for original MDPs; continuous-state extensions in are empirically illustrated without theoretical guarantees. [SSZ20] use Bayesian confidence reasoning, while provides guaranteed lower bounds for optimal satisfaction probability.Source: §12.1 · p. 54

12.2. Formal Analysis of Partially-Observed SHS.

• Partially observed SHS remain sparsely studied; finite approximations, barrier functions, and perception-aware planning address verification, safety, or sensing, while scalable POMDP synthesis remains open.Finite approximations provide error bounds and convergence under additive Gaussian noise in dynamics and observations; side-channel vulnerabilities also motivate SHS security models.Source: §12.2 · pp. 54–55, §12.3 · p. 55

12.3. Secure-by-Construction Controller Synthesis.

• Security requirements are often checked after controller design, motivating synthesis that integrates security with safety from the outset.The proposed direction generalizes correct-by-construction synthesis to include security requirements during controller design.Source: §12.3 · p. 56

12.4. (Mix)-monotonicity of SHS.

• Under stated noise and independence assumptions, mix-monotonicity can make computing IMC/IMDP transition-probability bounds more efficient.The approach uses the mix-monotonicity of the deterministic map to compute lower and upper bounds.Source: §12.4 · p. 56

12.5. Compositional Construction of IMCs/IMDPs.

• Compositional construction is a proposed way to mitigate IMC/IMDP complexity by building abstractions for high-dimensional systems from smaller subsystems.Source: §12.5 · p. 56

12.6. Compositional Controller Synthesis for SHS.

• A key open question is how local-controller satisfaction probabilities relate to the optimal probability for the interconnected system.Source: §12.6 · p. 56

12.7. Extensions and Development of Software Tools.

• Software development remains open for scalable continuous-time stochastic hybrid systems, infinite-horizon specifications, and compositional finite-MDP construction.Most surveyed tools target discrete-time models; the Level-Set Toolbox supports analysis of continuous-time models.Source: §12.7 · p. 56

• The article presents the first survey of automated formal verification and control synthesis for stochastic hybrid systems.Source: §13 · p. 57
• It distinguishes discretization-based from discretization-free approaches and examines four closeness guarantees between concrete systems and abstractions.Source: §13 · p. 57
• The survey covers methods, applications, software tools, and open problems, aiming to help readers understand SHS foundations and existing solutions.Source: §13 · p. 57