{"id":"782b7b62-1864-42ed-8471-52d5164b62fa","arxiv_id":"2503.04762","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"The paper shows that probabilistic STL verification for nonlinear stochastic systems can be reduced to deterministic verification of an eroded STL formula, with the erosion radius set by a deviation bound.","lead":"This paper presents a way to verify that a noisy robot or control system satisfies a time-sensitive safety rule: check a noiseless version of the system against a deliberately tightened version of the rule. The value is that ordinary deterministic verification tools can then give probabilistic safety guarantees for nonlinear stochastic systems.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The unicycle example (Sec. IV-B) erodes predicates using r=0.63 derived from a Lipschitz constant 'estimated by sampling'; without a certified global L_t, the claimed 1−10^−4 guarantee is unproven.","rationale":"The paper's main theorem is a conditional statement: if the deterministic system satisfies the eroded formula φ̃, then the stochastic system satisfies φ with 1−δ. The proof is an induction over STL operators and appears correct. The only input that can invalidate the conclusion is the erosion radius rδ,t, which must be a valid high-probability bound on the deviation. This bound is constructed from the global Lipschitz constants L_t. For the linear double-integrator example, L_t can be computed exactly from the matrices and controller, so that example is sound. For the nonlinear unicycle, however, the paper states the Lipschitz constant is 'estimated by sampling.' This is not a formal bound and, more importantly, the closed-loop system may not be globally Lipschitz at all. Thus the computed r=0.63 is not a certified PRS radius, and the claimed 1−10^−4 guarantee is not rigorously established. This is a weakness in the experimental validation of the paper's claimed generality to nonlinear systems, not in the theoretical reduction itself. The reader identified the same load-bearing assumption. A concrete check: compute a certified Lipschitz bound (or prove global Lipschitz fails) and re-evaluate the example. If the sampled estimate is confirmed, the example stands; if not, the conditional verdict remains warranted.","tokens_in":10531,"tokens_out":7486,"duration_ms":66421,"concrete_test":"Recompute the unicycle example with a certified global Lipschitz constant: use interval arithmetic or Lipschitz-certification tools to upper-bound L_t of the closed-loop map (13) with the given feedback controller on R^3 (or prove no finite L exists). Then recompute rδ,t from Theorem 3 using that bound and rerun the CORA verification of φ̃. If the certified L exceeds the sampled estimate and the verification fails (or the eroded safe sets become empty), the 1−10^−4 guarantee for Sec. IV-B is not established; if the certified L is no larger and verification still passes, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 3's guarantee depends on the erosion radius rδ,t, which is computed from the global Lipschitz constants L_t of the closed-loop dynamics (Assumption 1, Prop. 2). In Sec. IV-B the paper states 'The Lipschitz constant is estimated by sampling.' Sampling does not certify a global upper bound; it only provides a data-dependent estimate. For the nonlinear unicycle with feedback controller, the closed-loop map is not obviously globally Lipschitz on R^3: the controller contains terms such as Kx cosθ(p*_x−p_x), whose derivative with respect to θ grows with the position error, so the true global Lipschitz constant may be infinite. If the actual Lipschitz constant is larger than the estimate (or infinite), the computed radius rδ,t=0.63 is too small, the eroded predicates are too large, and the deterministic verification of φ̃ does not imply the advertised 1−10^−4 probabilistic satisfaction. Thus the paper's only nonlinear demonstration does not support its central claim for nonlinear systems; the correctness of the reduction itself is not in question, but the example's soundness is.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":10732,"tokens_out":7408,"duration_ms":72391,"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":[{"comment":"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":"Section IV-B (Nonlinear Unicycle)"},{"comment":"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.","section":"Section III-B (Proposition 2 and Theorem 3)"}],"minor_comments":[{"comment":"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 \tilde{E}_θ defined in equation (8), not to Eθ,T.","section":"Theorem 1 proof"},{"comment":"The notation \tilde{E}_θ is used both for the union set in (7) and for the product set in (8), and the suffix notation \tilde{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":"Section III-A (equations (7)–(8))"},{"comment":"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":"Section IV"},{"comment":"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":"Section II-B, Assumption 2"},{"comment":"The proof writes '(C ⊖ \tilde{E}_{θ,t}) ⊕ \tilde{E}_θ ⊆ C', but only \tilde{E}_θ has been defined; it should read '(C ⊖ \tilde{E}_θ) ⊕ \tilde{E}_θ ⊆ C' to match the statement of Proposition 1.","section":"Section III-A, Proposition 1 proof"}],"recommendation":"major_revision","confidential_remarks":"The paper's central reduction is sound, but its quantitative core is Proposition 2, quoted from the authors' own unpublished preprint [22]. I would ask the editor to confirm the status of [22] and, if possible, have the deviation bound independently checked, since Theorem 3 inherits all of its constants from that result. The nonlinear example also needs a certified Lipschitz constant rather than a sample-based estimate; this is a fixable but essential revision. The paper is otherwise a good fit for a formal verification journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat 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.\n\nThe 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.\n\nOne 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.\n\nWho 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.","headline":"Sound reduction from stochastic to deterministic STL verification, with a real but fixable gap in the nonlinear example's certified Lipschitz constant.","tokens_in":11273,"tokens_out":2386,"would_cite":true,"duration_ms":20835,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["signal temporal logic","stochastic systems","safety verification","probabilistic reachable set","predicate erosion","sub-Gaussian noise","reachability analysis","formal verification"],"falsifier":"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.","tokens_in":10306,"feed_emoji":"🛡️","tokens_out":8428,"duration_ms":71502,"temperature":0.7,"pith_summary":"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.","feed_headline":"Random-noise safety checks now reduce to deterministic reachability","feed_subtitle":"For nonlinear systems with sub-Gaussian noise, verifying a shrunk temporal-logic formula guarantees the original with probability 1−δ.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the deviation bound (Proposition 2) that determines the PRS radius $r_{\\delta,t}$, the quantitative core of the erosion strategy.","marker":"[22]"},{"why":"Introduces the set-erosion idea for safe-set specifications that the STL erosion strategy extends from sets to temporal formulas.","marker":"[15]"},{"why":"Extends the deviation bound to weighted norms, which the experiments use to get smaller Lipschitz constants and ellipsoidal PRS.","marker":"[27]"},{"why":"Previous predicate-tightening method restricted to affine predicates and linear systems; the paper's Proposition 1 generalizes it.","marker":"[19]"},{"why":"Deterministic STL model-checking algorithm used to verify the eroded formula in the numerical examples.","marker":"[8]"}],"fun_headline_variants":["Erosion strategy turns stochastic verification deterministic","Check a shrunk STL formula to certify stochastic safety","Stochastic STL satisfaction proven via deterministic erosion","Deterministic check ensures probabilistic STL compliance","Noise-free reachability with eroded spec guarantees STL"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Erosion strategy turns stochastic verification deterministic","Check a shrunk STL formula to certify stochastic safety","Stochastic STL satisfaction proven via deterministic erosion","Deterministic check ensures probabilistic STL compliance","Noise-free reachability with eroded spec guarantees STL"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000175,"raw_usage":{"total_tokens":1264,"prompt_tokens":902,"completion_tokens":362,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":289}},"tokens_in":518,"tokens_out":362,"duration_ms":3982,"temperature":1.0,"reasoning_tokens":289,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T13:27:32.275216+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Probabilistic Reachability of Discrete-Time Nonlinear Stochastic Systems","cited_arxiv_id":"2409.09334","evidence_quote":"Supplies the deviation bound (Proposition 2) that determines the PRS radius $r_{\\delta,t}$, the quantitative core of the erosion strategy."},{"cited_title":"Safety Verification of Stochastic Systems: A Set-Erosion Approach","cited_arxiv_id":"2410.02107","evidence_quote":"Introduces the set-erosion idea for safe-set specifications that the STL erosion strategy extends from sets to temporal formulas."},{"cited_title":"Stl model checking of continuous and hybrid systems,","cited_arxiv_id":null,"evidence_quote":"Deterministic STL model-checking algorithm used to verify the eroded formula in the numerical examples."}],"review_version":1}