Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications

Hongzhe Yu; Liqian Ma; Yongxin Chen; Zishun Liu

REVIEW 2 major objections 5 minor 31 references

Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications

T0 review · 2 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that probabilistic STL satisfaction for stochastic nonlinear systems can be verified by checking a noise-free system against an eroded STL formula, with the erosion radius set by a probabilistic reachable set bound.

desk verdict Sound reduction from stochastic to deterministic STL verification, with a real but fixable gap in the nonlinear example's certified Lipschitz constant. read the letter →

arxiv 2503.04762 v1 pith:7UCUB6TE submitted 2025-02-11 cs.LO cs.FLcs.SYeess.SY

Liqian Ma , Zishun Liu , Hongzhe Yu , Yongxin Chen This is my paper · ORCID

classification cs.LOcs.FLcs.SYeess.SY

keywords signaltemporallogicstochasticsystemssafetyverificationprobabilisticreachablesetpredicateerosionsub-Gaussiannoisereachabilityanalysisformal

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper proposes an STL erosion strategy for verifying that a discrete-time stochastic nonlinear system satisfies a signal temporal logic specification with probability at least $1-\delta$. The idea is to verify a noise-free version of the system against a tightened formula: each predicate's superlevel set is eroded by a probabilistic reachable set of the stochastic fluctuation, and the erosion radius is set by a sub-Gaussian deviation bound. If the deterministic system satisfies the eroded formula, the stochastic system is guaranteed to satisfy the original formula with the required probability. This converts a probabilistic temporal-logic verification problem into an ordinary deterministic reachability problem, with no need for linear dynamics or affine predicates. The bound grows only logarithmically in the horizon and confidence, so the approach remains usable for long horizons and small probability tolerances.

What carries the argument

The central object is the probabilistic reachable set (PRS) of the stochastic fluctuation, $E_{\theta,t}$, a set containing $e_t=X_t-x_t$ with probability at least $1-\theta$ for every initial state and disturbance sequence. The erosion step forms $\tilde{E}_\theta = \bigcup_{t=0}^{T} E_{\theta,t}$ and shrinks every predicate superlevel set $C$ to $C \ominus \tilde{E}_\theta$, so that any deterministic state satisfying the eroded predicate keeps the stochastic state inside $C$ no matter which fluctuation in $\tilde{E}_\theta$ occurs. The union bound over the $T$ time steps converts the per-step failure probability $\theta$ into the total tolerance $\delta=T\theta$. The deviation bound of Proposition 2 gives the concrete ball of radius $r_{\delta,t}$ as the PRS, and Theorem 3 plugs that radius into the erosion scheme, yielding a purely deterministic reachability check.

What would settle it

Run the unicycle example with the Lipschitz constant computed by a certified method (for example interval arithmetic) rather than by sampling; if the certified constants are larger, recompute $r_{\delta,t}$, and if the eroded formula then fails the deterministic verification, the claimed $1-10^{-4}$ guarantee does not follow. A more direct test is to compare the empirical $1-\delta$ quantile of $\|X_t-x_t\|$ from many simulations against the radius $r_{\delta,t}$: any significant exceedance would falsify the deviation bound that Theorem 3 depends on.

Watch

Extended reading notes

Core claim

The central claim is Theorem 3: for the discrete-time stochastic system $X_{t+1}=f(X_t,d_t,t)+w_t$ with sub-Gaussian noise $w_t$ and bounded disturbance $d_t$, under a global Lipschitz assumption on $f$, checking the noise-free system (3) against the eroded formula $\tilde{\varphi}$ implies that the stochastic system satisfies $\varphi$ with probability at least $1-\delta$. The eroded formula is obtained by replacing each predicate superlevel set $C$ with $C \ominus \tilde{E}_\theta$, where $\tilde{E}_\theta$ is the union over the horizon of probabilistic reachable sets of the fluctuation $e_t=X_t-x_t$, and $\theta=\delta/T$. Using the deviation bound from Proposition 2, the erosion radius is $r_{\delta,t} = \sqrt{\Psi_t(\varepsilon_1 n + \varepsilon_2 \log(T/\delta))}$, which makes the method applicable to nonlinear dynamics and non-affine predicates, in contrast to earlier tube-based STL methods that required linear dynamics or affine predicates. The paper validates the reduction on a double integrator and a nonlinear unicycle, with all $10^5$ sampled stochastic trajectories satisfying the specification in each case.

Load-bearing premise

The load-bearing premise is that the global Lipschitz constants $L_t$ of the closed-loop dynamics are known and certified; the nonlinear unicycle example estimates them by sampling, which does not certify an upper bound, and an underestimate would erode the predicates too much and break the $1-\delta$ guarantee.

Editorial extensions

If this is right

Any existing deterministic STL verification algorithm can be used unchanged, so progress in deterministic reachability transfers directly to stochastic verification.
Because $r_{\delta,t}$ scales logarithmically with $T$ and $1/\delta$, the method stays practical for long horizons and very small tolerances, where naive worst-case analysis fails.
The reduction removes the need for linear dynamics and affine predicates, extending probabilistic STL verification to a broad class of nonlinear models.
Worst-case erosion is strictly more conservative: in the unicycle example the worst-case radius is about 6.91 versus 0.63 for the stochastic bound, so the proposed method succeeds where worst-case analysis returns false.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Beyond the paper, any concentration inequality that yields a uniform-in-time probabilistic reachable set could be substituted for the sub-Gaussian bound, making the erosion strategy a general template rather than a bound-specific construction.
Beyond the paper, the same predicate erosion could be applied to quantitative robustness semantics of STL, yielding a certified probabilistic robustness margin; the paper only treats boolean satisfaction.
Beyond the paper, the main remaining conservatism is the union bound over time; replacing it with a path-wise concentration argument would shrink the erosion radius further and could be tested against the same examples.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The short version: the core reduction is sound and genuinely useful, but the nonlinear numerical example has a load-bearing gap that should be fixed before the headline guarantee is taken at face value.

What is new: prior work by this group eroded safe sets; here they extend the same idea to full STL formulas with temporal operators. For each predicate, they erode the superlevel set by the union of probabilistic reachable sets of the deviation between stochastic and deterministic trajectories. Theorem 1's induction over STL operators is correct, and Theorem 3 instantiates it with a deviation bound from their companion paper [22]. The result is that probabilistic STL verification for discrete-time nonlinear systems reduces to deterministic verification, with no linear-dynamics or affine-predicate restriction, and it can ride on existing tools like CORA. That is a solid contribution.

The double integrator example is fine. The unicycle example is the problem. They say the Lipschitz constant of the closed-loop map is 'estimated by sampling.' That constant feeds directly into the erosion radius r_{δ,t}; if the estimate is too small, the eroded predicates are too large, and the claimed 1−10^−4 guarantee does not follow. Sampling does not certify a global upper bound, and the feedback controller here is not obviously globally Lipschitz on R^3—the derivative with respect to θ grows with position error. So the only nonlinear demonstration does not actually support the nonlinear claim as stated. This is fixable: use a certified Lipschitz bound on a bounded domain, or derive a local constant from the reachable set, or switch to a controller with a provable global Lipschitz constant.

One more dependency: the quantitative engine, Proposition 2, is quoted from [22], not re-derived. That is acceptable for a paper like this, as long as the referee checks the statement matches the source.

Who should read it: anyone working on probabilistic verification of temporal-logic properties for stochastic systems. It gives a clean framework and a clear path to implementation. It deserves a serious referee; the reduction theorem is worth publishing, and the example can be fixed with honest effort.

Referee Report

2 major / 5 minor

Summary. The paper proposes a reduction for probabilistic STL verification of discrete-time stochastic systems with bounded deterministic disturbances and sub-Gaussian noise. The main idea is to erode every predicate in the STL formula by a probabilistic reachable set of the stochastic fluctuation, so that if the deterministic trajectory satisfies the eroded formula, then the stochastic trajectory satisfies the original formula with probability at least 1−δ. The erosion radius is derived from a deviation bound quoted from the authors' prior work [22]. The paper proves the reduction in Theorems 1–3 and demonstrates it on a linear double-integrator example and a nonlinear unicycle example, with CORA used for deterministic verification.

Significance. If the result is correct, the paper gives a clean and broadly applicable reduction: probabilistic STL verification for nonlinear systems under sub-Gaussian noise is reduced to deterministic STL verification, without requiring linear dynamics or affine predicates. The central proof of the reduction (Proposition 1 and Theorem 1) is elementary and, modulo a few notational slips, correct. The paper also includes a useful comparison showing that the proposed bound is less conservative than the earlier worst-case bound. However, the quantitative engine of the method is Proposition 2, quoted from unpublished prior work, and the only nonlinear numerical example does not currently certify the global Lipschitz assumption on which the guarantee rests. These issues are fixable, but they need to be addressed before the paper can fully support its claims.

major comments (2)

[Section IV-B (Nonlinear Unicycle)] Assumption 1 and Proposition 2 require certified global Lipschitz constants L_t for all x,y∈R^3 and d∈D, but the text states 'The Lipschitz constant is estimated by sampling.' For the closed-loop unicycle with the given tracking controller, the dynamics contain terms such as K_x cosθ(p*_x−p_x) and K_y sinθ(p*_y−p_y), whose derivatives with respect to θ grow with the position error. The closed-loop map is therefore not evidently globally Lipschitz on R^3, and a sample-based estimate cannot certify a global upper bound. If the true Lipschitz constant is larger than the sampled estimate, the computed radius rδ,t=0.63 is too small, the eroded predicates are too large, and the claimed 1−10^−4 probabilistic guarantee does not follow from Theorem 3. Since the unicycle is the paper's only nonlinear demonstration, this is a load-bearing gap. The authors should replace the sampled estimate with a certified global or compact-domain Lipschitz bound, for example by restricting to a forward-invariant compact set and computing an interval-arithmetic or optimization-based bound on that set.
[Section III-B (Proposition 2 and Theorem 3)] Theorem 3's guarantee depends entirely on Proposition 2, which is quoted from the authors' unpublished preprint [22] without proof or a precise statement of its hypotheses. In particular, the definitions of ε1 and ε2, the role of the free parameter ε, and the exact conditions under which the weighted-norm version ∥·∥_P holds are stated only cryptically in the text and in a pointer to [27, Section V-D]. Since these constants determine the erosion radius rδ,t, the reader cannot independently verify the most important quantitative ingredient of the method. The authors should either include a proof or a complete statement of the needed deviation bound in an appendix, or clearly state the exact theorem from [22] together with all assumptions needed for Theorem 3.

minor comments (5)

[Theorem 1 proof] The final line of the proof says 'x[0,T]+e[0,T] |= φ, ∀e[0,T] ∈ Eθ,T', but should refer to the product set ilde{E}_θ defined in equation (8), not to Eθ,T.
[Section III-A (equations (7)–(8))] The notation ilde{E}_θ is used both for the union set in (7) and for the product set in (8), and the suffix notation ilde{E}_θ[t,T] used in the proof of Theorem 1 is never defined. Please clarify these definitions, since the until-case of the induction relies on suffix products.
[Section IV] The examples define predicates such as π_goal via inequalities of the form µ(x)≤0, while the formal definition in Section II-A defines a predicate as µ(x)≥0. Please state explicitly that inequalities are normalized by negating µ, or consistently use either superlevel or sublevel sets.
[Section II-B, Assumption 2] Assumption 2 states σ_t>0 for all t>0, but the dynamics (2) involve w_t with t starting at 0; the assumption should cover t≥0 (or the convention should be stated) so that the initial noise term is not omitted.
[Section III-A, Proposition 1 proof] The proof writes '(C ⊖ ilde{E}_{θ,t}) ⊕ ilde{E}_θ ⊆ C', but only ilde{E}_θ has been defined; it should read '(C ⊖ ilde{E}_θ) ⊕ ilde{E}_θ ⊆ C' to match the statement of Proposition 1.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the reduction theorem is proven in the paper, and the cited deviation bound is an independent concentration result with separate assumptions.

full rationale

The paper's central contribution is Theorem 1/2, which shows that if a deterministic trajectory satisfies an STL formula with predicates eroded by a probabilistic reachable set (PRS), then the associated stochastic trajectory satisfies the original formula with probability at least 1−Tθ. This proof is carried out in the paper via induction and only uses the definition of a PRS and the union bound; it does not assume its own conclusion. The specific PRS (ball of radius rδ,t) is supplied by Proposition 2, quoted from the authors' prior work [22]. That cited result is a concentration bound for sub-Gaussian noise under a global Lipschitz assumption; it is parameter-free, its assumptions do not include the STL verification statement, and it is not a restatement of Theorem 3. Thus Theorem 3 follows by substitution, not by circular reasoning. The numerical unicycle example estimates the global Lipschitz constant by sampling, which is a soundness gap if the estimate is not certified; however, this is a limitation of the example, not a case of a fitted parameter being renamed as a prediction. The deterministic verification is performed independently by CORA, and the probabilistic guarantee is a logical consequence of the stated Lipschitz bound, not of the sampled validation trajectories. No equation in the paper reduces to its own input by construction.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The verification guarantee is an assembly of three load-bearing ingredients: global Lipschitz constants for the dynamics, sub-Gaussian noise, and the deviation bound of [22] which is quoted as a black box. The nonlinear example adds a non-certified Lipschitz estimate. No new ontological entities are introduced.

free parameters (1)

Global Lipschitz constants L_t of the closed-loop dynamics in the unicycle example = not reported, estimated by sampling
Section IV-B: "The Lipschitz constant is estimated by sampling." The PRS radius rδ,t depends on Ψ_t = product of L_k^2; an underestimate shrinks the erosion radius and voids the 1-δ guarantee.

assumptions (5)

domain assumption Assumption 1: f is globally Lipschitz with known constants L_t for all t.
Required for Proposition 2's concentration bound; the paper estimates L_t by sampling in the unicycle example, which does not certify a global bound (Section IV-B).
domain assumption Assumption 2: each stochastic disturbance w_t is zero-mean sub-Gaussian with variance proxy σ_t^2.
Needed for the deviation bound in Proposition 2; the examples use Gaussian noise, which is sub-Gaussian.
domain assumption Proposition 2 from [22]: P(∥Xt−xt∥ ≤ rθ,t) ≥ 1−θ for the stated radius rθ,t.
The paper quotes this bound without proof and uses it as the size of the eroded predicates; the whole verification guarantee inherits the correctness of this cited result.
standard math STL formulas can be converted to negation-free form with reversed-inequality predicates.
Used in Section II-A to avoid handling negation in the erosion induction; the conversion is cited to [24] and [26] and is standard.
standard math Minkowski difference satisfies (C ⊖ B) ⊕ B ⊆ C.
Used in Proposition 1 to guarantee that eroding predicates by ~Eθ keeps the state inside the original predicate after adding any fluctuation in ~Eθ.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications." pith.science (2026). https://pith.science/paper/7UCUB6TE

@misc{pith2026250304762,
  author       = {Pith},
  title        = {Pith review of: Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7UCUB6TE}},
  note         = {Machine review of arXiv:2503.04762}
}

read the original abstract

We study the verification problem of stochastic systems under signal temporal logic (STL) specifications. We propose a novel approach that enables the verification of the probabilistic satisfaction of STL specifications for nonlinear systems subject to both bounded deterministic disturbances and stochastic disturbances. Our method, referred to as the STL erosion strategy, reduces the probabilistic verification problem into a deterministic verification problem with a tighter STL specification. The degree of tightening is determined by leveraging recent results on bounding the deviation between the stochastic trajectory and the deterministic trajectory. Our approach can be seamlessly integrated with any existing deterministic STL verification algorithm. Numerical experiments are conducted to showcase the efficacy of our method.

Figures

Figures reproduced from arXiv: 2503.04762 by the authors.

**Figure 3.** Stochastic STL verification of the unicycle system with [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

**Figure 2.** Stochastic STL verification of the double integrator system (12) with [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 25 canonical work pages

[22]

Probabilistic Reachability of Discrete-Time Nonlinear Stochastic Systems

Z. Liu, S. Jafarpour, and Y . Chen, “Probabilistic reachabil- ity of discrete-time nonlinear stochastic systems,” arXiv preprint arXiv:2409.09334, 2024

work page Pith review arXiv 2024
[1]

Safety and security in cyber-physical systems and internet-of-things systems,

M. Wolf and D. Serpanos, “Safety and security in cyber-physical systems and internet-of-things systems,” Proceedings of the IEEE, vol. 106, no. 1, pp. 9–20, 2017

work page 2017
[2]

Safety-critical advanced robots: A survey,

J. Guiochet, M. Machin, and H. Waeselynck, “Safety-critical advanced robots: A survey,” Robotics and Autonomous Systems , vol. 94, pp. 43– 52, 2017

work page 2017
[3]

Safety assessment of collaborative robotics through automated formal veri- fication,

F. Vicentini, M. Askarpour, M. G. Rossi, and D. Mandrioli, “Safety assessment of collaborative robotics through automated formal veri- fication,” IEEE Transactions on Robotics , vol. 36, no. 1, pp. 42–61, 2019

work page 2019
[4]

Safety verification of hybrid systems using barrier certificates,

S. Prajna and A. Jadbabaie, “Safety verification of hybrid systems using barrier certificates,” in International Workshop on Hybrid Systems: Computation and Control . Springer, 2004, pp. 477–492

work page 2004
[5]

Monitoring temporal properties of con- tinuous signals,

O. Maler and D. Nickovic, “Monitoring temporal properties of con- tinuous signals,” in International symposium on formal techniques in real-time and fault-tolerant systems . Springer, 2004, pp. 152–166

work page 2004
[6]

Hamilton-jacobi reachability: A brief overview and recent advances,

S. Bansal, M. Chen, S. Herbert, and C. J. Tomlin, “Hamilton-jacobi reachability: A brief overview and recent advances,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) . IEEE, 2017, pp. 2242–2253

2017
[7]

Signal temporal logic meets reachability: Connections and applications,

M. Chen, Q. Tam, S. C. Livingston, and M. Pavone, “Signal temporal logic meets reachability: Connections and applications,” in Interna- tional Workshop on the Algorithmic Foundations of Robotics. Springer, 2018, pp. 581–601

work page 2018

Show all 31 references

[8]

Stl model checking of continuous and hybrid systems,

H. Roehm, J. Oehlerking, T. Heinz, and M. Althoff, “Stl model checking of continuous and hybrid systems,” in Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings 14 . Springer, 2016, pp. 412–427

2016
[9]

Using four-valued signal temporal logic for incremental verification of hybrid systems,

F. Lercher and M. Althoff, “Using four-valued signal temporal logic for incremental verification of hybrid systems,” in International Con- ference on Computer Aided Verification. Springer, 2024, pp. 259–281

2024
[10]

Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis,

N. Kochdumper and S. Bak, “Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis,” Nonlinear Analysis: Hybrid Systems , vol. 53, p. 101491, 2024

2024
[11]

Finite-time regional verification of stochastic non-linear systems,

J. Steinhardt and R. Tedrake, “Finite-time regional verification of stochastic non-linear systems,” The International Journal of Robotics Research, vol. 31, no. 7, pp. 901–923, 2012

2012
[12]

A barrier function approach to finite-time stochastic system verification and control,

C. Santoyo, M. Dutreix, and S. Coogan, “A barrier function approach to finite-time stochastic system verification and control,” Automatica, vol. 125, p. 109439, 2021

2021
[13]

Collision probabilities for continuous-time systems without sampling [with appendices],

K. M. Frey, T. J. Steiner, and J. P. How, “Collision probabilities for continuous-time systems without sampling [with appendices],” arXiv preprint arXiv:2006.01109, 2020

2006 arXiv
[14]

Monte carlo motion plan- ning for robot trajectory optimization under uncertainty,

L. Janson, E. Schmerling, and M. Pavone, “Monte carlo motion plan- ning for robot trajectory optimization under uncertainty,” in Robotics Research: Volume 2. Springer, 2017, pp. 343–361

2017
[15]

Safety verification of stochastic systems: A set-erosion approach,

Z. Liu, S. Jafarpour, and Y . Chen, “Safety verification of stochastic systems: A set-erosion approach,” arXiv preprint arXiv:2410.02107 , 2024

2024 arXiv
[16]

Safe control under uncertainty with proba- bilistic signal temporal logic,

D. Sadigh and A. Kapoor, “Safe control under uncertainty with proba- bilistic signal temporal logic,” in Proceedings of Robotics: Science and Systems XII, 2016

2016
[17]

Shrinking horizon model predictive control with signal temporal logic constraints under stochastic disturbances,

S. S. Farahani, R. Majumdar, V . S. Prabhu, and S. Soudjani, “Shrinking horizon model predictive control with signal temporal logic constraints under stochastic disturbances,” IEEE Transactions on Automatic Con- trol, vol. 64, no. 8, pp. 3324–3331, 2018

2018
[18]

Distributed model predictive control for probabilistic signal temporal logic specifications,

T. Yang, Y . Zou, S. Li, and Y . Yang, “Distributed model predictive control for probabilistic signal temporal logic specifications,” IEEE Transactions on Automation Science and Engineering , 2023

2023
[19]

Probabilistic tube-based control synthesis of stochastic multi-agent systems under signal temporal logic,

E. E. Vlahakis, L. Lindemann, P. Sopasakis, and D. V . Dimarogonas, “Probabilistic tube-based control synthesis of stochastic multi-agent systems under signal temporal logic,”arXiv preprint arXiv:2405.02827, 2024

2024 arXiv
[20]

Control barrier functions for stochastic systems under signal temporal logic tasks,

A. B. Kordabad, M. Charitidou, D. V . Dimarogonas, and S. Soudjani, “Control barrier functions for stochastic systems under signal temporal logic tasks,” in 2024 European Control Conference (ECC) . IEEE, 2024, pp. 3213–3219

2024
[21]

Data-driven verification of stochastic linear systems with signal temporal logic constraints,

A. Salamati, S. Soudjani, and M. Zamani, “Data-driven verification of stochastic linear systems with signal temporal logic constraints,” Automatica, vol. 131, p. 109781, 2021

2021
[23]

Theory and computation of dis- turbance invariant sets for discrete-time linear systems,

I. Kolmanovsky and E. G. Gilbert, “Theory and computation of dis- turbance invariant sets for discrete-time linear systems,” Mathematical problems in engineering , vol. 4, no. 4, pp. 317–367, 1998

1998
[24]

Formal methods for control synthesis: An optimization perspective,

C. Belta and S. Sadraddini, “Formal methods for control synthesis: An optimization perspective,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 115–140, 2019

2019
[25]

Robustness of temporal logic spec- ifications for continuous-time signals,

G. E. Fainekos and G. J. Pappas, “Robustness of temporal logic spec- ifications for continuous-time signals,” Theoretical Computer Science , vol. 410, no. 42, pp. 4262–4291, 2009

2009
[26]

Robust temporal logic model predictive control,

S. Sadraddini and C. Belta, “Robust temporal logic model predictive control,” in 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton) . IEEE, 2015, pp. 772–779

2015
[27]

Probabilistic reachability analysis of stochastic control systems,

S. Jafarpour, Z. Liu, and Y . Chen, “Probabilistic reachability analysis of stochastic control systems,” arXiv preprint arXiv:2407.12225, 2024

2024 arXiv
[28]

A framework for worst- case and stochastic safety verification using barrier certificates,

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 , vol. 52, no. 8, pp. 1415–1428, 2007

2007
[29]

Signal temporal logic neural predictive control,

Y . Meng and C. Fan, “Signal temporal logic neural predictive control,” IEEE Robotics and Automation Letters , 2023

2023
[30]

Simulation-driven reacha- bility using matrix measures,

C. Fan, J. Kapinski, X. Jin, and S. Mitra, “Simulation-driven reacha- bility using matrix measures,” ACM Transactions on Embedded Com- puting Systems (TECS) , vol. 17, no. 1, pp. 1–28, 2017

2017
[31]

An introduction to CORA 2015,

M. Althoff, “An introduction to CORA 2015,” in Proc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems. EasyChair, December 2015, pp. 120–151. [Online]. Available: https://easychair.org/publications/paper/xMm

2015

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.

[1] [22]

Probabilistic Reachability of Discrete-Time Nonlinear Stochastic Systems

Z. Liu, S. Jafarpour, and Y . Chen, “Probabilistic reachabil- ity of discrete-time nonlinear stochastic systems,” arXiv preprint arXiv:2409.09334, 2024

work page Pith review arXiv 2024

[2] [1]

Safety and security in cyber-physical systems and internet-of-things systems,

M. Wolf and D. Serpanos, “Safety and security in cyber-physical systems and internet-of-things systems,” Proceedings of the IEEE, vol. 106, no. 1, pp. 9–20, 2017

work page 2017

[3] [2]

Safety-critical advanced robots: A survey,

J. Guiochet, M. Machin, and H. Waeselynck, “Safety-critical advanced robots: A survey,” Robotics and Autonomous Systems , vol. 94, pp. 43– 52, 2017

work page 2017

[4] [3]

Safety assessment of collaborative robotics through automated formal veri- fication,

F. Vicentini, M. Askarpour, M. G. Rossi, and D. Mandrioli, “Safety assessment of collaborative robotics through automated formal veri- fication,” IEEE Transactions on Robotics , vol. 36, no. 1, pp. 42–61, 2019

work page 2019

[5] [4]

Safety verification of hybrid systems using barrier certificates,

S. Prajna and A. Jadbabaie, “Safety verification of hybrid systems using barrier certificates,” in International Workshop on Hybrid Systems: Computation and Control . Springer, 2004, pp. 477–492

work page 2004

[6] [5]

Monitoring temporal properties of con- tinuous signals,

O. Maler and D. Nickovic, “Monitoring temporal properties of con- tinuous signals,” in International symposium on formal techniques in real-time and fault-tolerant systems . Springer, 2004, pp. 152–166

work page 2004

[7] [6]

Hamilton-jacobi reachability: A brief overview and recent advances,

S. Bansal, M. Chen, S. Herbert, and C. J. Tomlin, “Hamilton-jacobi reachability: A brief overview and recent advances,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) . IEEE, 2017, pp. 2242–2253

2017

[8] [7]

Signal temporal logic meets reachability: Connections and applications,

M. Chen, Q. Tam, S. C. Livingston, and M. Pavone, “Signal temporal logic meets reachability: Connections and applications,” in Interna- tional Workshop on the Algorithmic Foundations of Robotics. Springer, 2018, pp. 581–601

work page 2018