{"id":"6ae0b3aa-6d61-4040-890b-c730405ab484","arxiv_id":"1909.00898","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new sound robustness score for continuous-time STL, AGIM, uses arithmetic and geometric integral means over all subformulae and times, and is demonstrated on falsification and multi-agent synthesis.","lead":"This paper introduces a new way to measure how robustly a continuous-time signal meets a Signal Temporal Logic specification, using averages over all times rather than a single worst moment. The method improves falsification and control synthesis for complex and multi-agent systems by giving optimizers more informative, smoother objectives.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Soundness of the implemented AGIM score is not established: Algorithm 1 requires an exact ANY test over a continuum, but Sections V–VI evaluate it on finite simulation samples, so short violations (the paper's own motivating failure mode) can be missed and the computed sign can disagree with STL…","rationale":"The reader's weakest assumption is the same one I would defend as most load-bearing: the ANY condition over a continuum is the linchpin that connects the mathematical soundness theorem to the algorithms and case studies. The paper's own motivating example rejects discretization, yet the implemented η inherits the same sampling limitation. I considered whether a deeper mathematical flaw exists: for arbitrary Lebesgue-integrable signals, a measure-zero violation makes η=0 while ρ<0, so Theorem 2 needs a regularity hypothesis such as left/right continuity. This strengthens rather than replaces the reader's concern, since both center on short violations failing to affect the computed score. The good-faith reading is that the definition is sign-sound for continuous trajectories from ODEs; the proofs are sketches but the G case indicates the intended induction. The missing piece is a procedure or restriction that makes the continuum ANY test computable or approximable with guarantees. That is a concrete conditional acceptance criterion, not a rejection: the mathematical idea is coherent and the experiments are suggestive, but they do not yet establish the continuous-time advantage over discrete-time robustness. No code is provided, so the sampling behavior cannot be checked independently, which is another reason the verification step is appropriate.","tokens_in":12955,"tokens_out":21026,"duration_ms":235122,"concrete_test":"Run the Section VI falsification benchmark with a fixed simulation step h. Insert a violation of width w<h (e.g., RPM>4000 for 0.1 s) between two consecutive sample times in an otherwise safe trace. If Algorithm 1 on the sampled trace returns η≥0 whereas the true continuous-time φ_Falsify is violated, the computed score is not the sound AGIM of Theorem 2. A minimal reproduction is: s(t)=0 everywhere except s(0.5)=-0.1, φ=G[0,1](s≥0); Definition 2 gives η=0 while ρ=-0.1 unless left-continuity/positive-measure is assumed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 2 is stated for the exact AGIM robustness η, but the only evaluation procedure offered, Algorithm 1, branches on continuum ANY conditions, e.g., line 19 'ANY (η(ϕ,S,τ) ≤0) for τ∈[a,b]'. The paper gives no exact decision procedure for this test; Remark 1 only asserts that efficient representations 'exist.' In the falsification and synthesis experiments, η is computed from finite Simulink traces. Any violation whose duration is shorter than the sample spacing never appears in the ANY test, so the computed score can be positive while the continuous-time signal violates the formula. This is exactly the discretization failure the introduction attributes to discrete-time robustness, so the experimental pipeline does not deliver the advertised continuous-time soundness. A second, related gap is that the theorem's equivalence requires enough signal regularity for a violation to have positive measure and for strict pointwise positivity to imply a positive minimum; under the stated 'bounded Lebesgue integrable' assumption, a single-instant violation gives η=0 while ρ<0.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Arithmetic-Geometric Integral Mean (AGIM) robustness for continuous-time Signal Temporal Logic (STL), replacing the min/max operations of traditional robustness with operator-dependent arithmetic and geometric integral means. The score is normalized to the interval [−1, 1], and the paper claims that its sign is equivalent to the sign of traditional robustness, hence sound with respect to the usual STL satisfaction relation. The authors argue that averaging over the full signal and all subformulae avoids the masking effect and locality of the traditional score, and they demonstrate the approach on a Simulink automatic-transmission falsification benchmark and on multi-agent control synthesis problems with temporal tasks. Theorem 2 (soundness) is proved only by a sketch covering the Globally case, and several appealing properties (idempotence, commutativity, monotonicity, De Morgan laws, smoothness) are stated with proofs deferred to structural induction.","tokens_in":13180,"tokens_out":9607,"duration_ms":108730,"significance":"The core idea is attractive: an average-based, normalized, sign-sound robustness score is a principled way to make STL robustness more informative for optimization while preserving the meaning of satisfaction and violation. The paper explicitly states a soundness theorem against the independent traditional semantics, which is the right property to establish, and the falsification and synthesis case studies show that the score can distinguish signals that traditional robustness treats as equal. The main value would be in gradient-friendly falsification and control synthesis for continuous-time systems, where a sound score that uses more of the signal could improve optimization landscapes. However, the manuscript as written leaves a significant gap between the exact continuous-time definition, for which soundness is proved, and the finite-sample evaluation actually used in the experiments, and the soundness theorem itself is stated under regularity assumptions that are too weak for the claimed equivalence. The approach is promising and the central claims appear defensible after a substantial revision.","major_comments":[{"comment":"The exact AGIM score is defined via continuum ANY tests, for example whether there exists τ in [t+a, t+b] with η(ϕ,S,τ) ≤ 0, but the paper provides no exact decision procedure for such tests. Remark 1 only asserts that efficient representations exist. In the falsification and synthesis experiments, the robustness is evaluated on the finite time samples produced by the Simulink simulation and by the piecewise-constant input discretization in Eq. (8). A violation whose duration is shorter than the sampling spacing is invisible to the ANY test, so the computed score can be positive while the underlying continuous-time signal violates the formula. This is precisely the discretization failure that the motivating example (Fig. 1) attributes to discrete-time scores. Consequently, Theorem 2 proves soundness for the idealized exact η, but not for the quantity actually optimized in Sections V and VI. The authors should either implement an exact ANY test for the signal representation used or explicitly present the experimental score as an approximation whose soundness is not claimed.","section":"Algorithm 1, line 19; Sections V–VI"},{"comment":"The claimed equivalence η(ϕ,S,t) < 0 ⇔ ρ(ϕ,S,t) < 0 fails under the stated assumption that signals are bounded and Lebesgue integrable, because a predicate violation on a set of measure zero gives η = 0 while ρ < 0. The proof sketch's converse step, which infers the existence of τ with η(ϕ,τ) < 0 from ρ < 0, is not valid in this generality. The theorem should either assume enough regularity, e.g., continuous or one-sided continuous signals so that a negative robustness implies a violation of positive measure, or state only the one-sided implications η > 0 ⇒ ρ > 0 and η < 0 ⇒ ρ < 0.","section":"Theorem 2, Eq. (5); Section IV assumptions"},{"comment":"The central definition is not self-consistent as printed. In Eq. (4) and Algorithm 1, the G and F cases use the interval [a,b] in both the ANY condition and the integral bounds, whereas the syntax G[a,b]ϕ at time t and the proof sketch of Theorem 2 use [t+a, t+b]. As written, the score does not depend on t. Additionally, the STL syntax in Eq. (1) includes the Until operator, but Definition 2 and Algorithm 1 define no case for ϕ1 U[a,b] ϕ2, even though Theorem 2 is stated for arbitrary STL formulas. The authors should fix the time offset in the definition and either extend the robustness definition to Until or explicitly restrict the paper's claims to the F/G fragment.","section":"Eq. (4); Algorithm 1, lines 19–32; Eq. (1)"},{"comment":"The smoothness claims are load-bearing for the paper's motivation, since the score is proposed as an improvement for gradient-based optimization, but the proof sketch is not adequate. The claim that left-continuity implies only a countable set of discontinuities does not by itself establish differentiability almost everywhere of the recursively defined integrals, and the time-dependent interval endpoints in the G and F cases require a separate argument. The gradient-nonzero claim also should be stated with the precise conditions under which it holds. Provide complete proofs or weaken the claims to what is actually needed for the optimization experiments.","section":"Section IV-C, Smoothness Properties"}],"minor_comments":[{"comment":"The violation-branch integrals for both G and F contain the placeholder t'_k; this should be τ.","section":"Eq. (4)"},{"comment":"The statement 'η>0 ⇔ ρ>0 ⇒ S ⊨ ϕ' is ambiguous; use parentheses, e.g., 'η>0 iff ρ>0, and ρ>0 implies S ⊨ ϕ'.","section":"Theorem 2, Eq. (5)"},{"comment":"Remark 1 is too vague: it should name concrete dense-time monitoring algorithms or data structures that realize the ANY test exactly, since the paper's continuous-time claim depends on this.","section":"Remark 1"},{"comment":"The empirical comparisons are single-run examples without confidence intervals or repeated trials; Table I reports averages without variance, so the runtime and performance claims are not statistically supported.","section":"Section VI, Table I"},{"comment":"Section II allows arbitrary continuous predicates µ := l(S) ≥ 0, but Definition 2 only defines the AGIM score for predicates of the form si ≥ π; the syntax and the robustness definition should be reconciled.","section":"Section II and Definition 2"},{"comment":"Reference [21] lists 'H. A. Bardh Hoxha and G. Fainekos'; verify the author list, which appears malformed.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper's central idea is salvageable and the soundness property is the right one to claim, but the mismatch between the exact continuous-time definition and the finite-sample experiments is serious, especially because the paper's own motivating example is about missing violations between samples. The authors should be asked to provide an exact monitoring procedure or clearly separate the experimental approximation, fix the regularity assumptions in Theorem 2, and complete the definition for all STL operators or explicitly restrict the scope. The novelty relative to the authors' prior discrete-time AGM work should also be clarified, though this is not, by itself, a blocking concern."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The AGIM robustness is a real addition to the STL toolkit. Pairing arithmetic means with F/∨ and geometric means with G/∧ is a well-motivated design that avoids the masking and locality of the standard min/max score and gives a normalized score that stays sign-sound in the sense that positive means satisfaction and negative means violation. That alone is a useful step beyond the discrete AGM and the earlier average-based scores, which either used arithmetic means only or lost soundness.\n\nThe paper is good at explaining the intuition: for an eventually, averaging the satisfying values rewards staying satisfying for longer, while for a globally, the geometric mean correctly weighs the worst near-violation. The falsification and multi-agent examples support the qualitative claim that the new score differentiates behaviors the traditional score cannot.\n\nBut the paper overclaims in two places. First, Theorem 2 states a biconditional: η>0 iff ρ>0 and η<0 iff ρ<0. The negative direction fails under the stated Lebesgue-integrable assumption for signals that are not continuous: a violation that occurs at a single instant gives η=0 while ρ<0. The paper calls η=0 inconclusive, which saves the implications but not the iff. If the authors assume continuity, they should say so and the theorem becomes cleaner. As written, the equivalence is false.\n\nSecond, and more important, Algorithm 1 requires an exact ANY test over a continuum, but the case studies clearly evaluate on finite Simulink samples. A violation shorter than the sample spacing is invisible, so the computed score can be positive while the continuous-time signal violates the formula. This is precisely the discretization failure the paper's own motivating example warns against. Remark 1 asserts that efficient representations exist, but no method is given and no code is released. The reader is left with a soundness theorem for an idealized score and an implementation that does not obviously inherit that soundness. That gap deserves a serious response.\n\nThe proofs are also sketches—only the G case is shown for Theorem 2, and the smoothness proof is asserted by induction. That might be acceptable in a conference, but for a theorem-driven paper it is thin. The experimental comparisons in Table I are useful but appear to be single-run numbers without statistics.\n\nI would send this to review. With a tightened theorem, a rigorous proof, and some discussion of the finite-sampling approximation—or an exact ANY for the chosen signal representation—the AGIM score could be a solid contribution. Right now it is a promising idea with overclaimed guarantees.","headline":"A promising average-based robustness score for continuous-time STL with a real definitional contribution, but the soundness theorem is overstated and the finite-sampling implementation falls short of the paper's own continuity claims.","tokens_in":13682,"tokens_out":4366,"would_cite":true,"duration_ms":48300,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proposes a new average-based STL robustness score, AGIM, that agrees with standard STL semantics in sign while using every time and subformula.","keywords":["Signal Temporal Logic","robustness","continuous-time signals","falsification","control synthesis","arithmetic-geometric mean","geometric integral","multi-agent systems"],"falsifier":"Run the AGIM algorithm on a continuous-time signal that contains a brief violation shorter than the implementation's sampling interval, such as a one-millisecond overshoot above the threshold in a step response sampled coarsely; if the sampled implementation returns a positive AGIM score for a Globally specification while the true continuous signal violates it, the practical soundness claim is falsified.","tokens_in":12781,"feed_emoji":"📊","tokens_out":6260,"duration_ms":66592,"temperature":0.7,"pith_summary":"The paper replaces the worst-point min/max robustness of Signal Temporal Logic with an average-based score called Arithmetic-Geometric Integral Mean (AGIM), defined for continuous-time signals. It claims that the new score is sound in the usual STL sense: a strictly positive score means the specification is satisfied, and a strictly negative score means it is violated. Unlike the traditional score, which is determined by a single most extreme time point or subformula, AGIM uses arithmetic and geometric integral means so that every time and every subformula contributes. The authors show that this gives a smoother, more informative objective for falsification and control synthesis, and they demonstrate this on an automotive benchmark and multi-agent examples.","feed_headline":"Average-based STL score stays sound and uses the whole signal","feed_subtitle":"Worst-point min/max scores ignore most of a signal; averaging over all times keeps soundness and helps falsification.","key_machinery":"The carrying object is the Arithmetic-Geometric Integral Mean score, built from two continuous averaging operations: the arithmetic integral mean $\\frac{1}{b-a}\\int_a^b f(\\tau)\\,d\\tau$ and the geometric integral mean $\\prod_a^b f(x)^{dx}=\\exp\\left(\\int_a^b \\ln f(x)\\,dx\\right)$, the continuous analog of a product. The key design choice is which mean is applied where: arithmetic means for disjunction and Eventually, where the total positive evidence matters, and geometric means for conjunction and Globally, where consistency across all times matters; negative evidence is averaged arithmetically. This split is what lets every subformula and every time contribute to the score while preserving sign-soundness with respect to the traditional semantics.","core_discovery":"The central claim is that a recursively defined average-based robustness $\\eta(\\phi,S,t)\\in[-1,1]$ is sound and strictly more informative than the traditional STL robustness $\\rho$. For predicates, $\\eta(\\mu,S,t)=\\tfrac{1}{2}(s_i(t)-\\pi)$; negation flips the sign; conjunction and Globally use the geometric integral of $(1+\\eta)$ when all subformulae are positive, otherwise average the negative parts; disjunction and Eventually use the arithmetic mean of positive parts when some part is positive, otherwise a negative geometric form. Theorem 2 states that $\\eta(\\phi,S,t)>0 \\iff \\rho(\\phi,S,t)>0$, and $\\eta(\\phi,S,t)<0 \\iff \\rho(\\phi,S,t)<0$, so the sign of AGIM always agrees with the standard STL satisfaction relation while its magnitude summarizes the entire signal rather than one extreme point.","pith_inferences":["Inference: a production-grade implementation of AGIM would need a certified way to evaluate the ANY conditions over continuous intervals, such as interval arithmetic or reachability analysis; otherwise the sampled implementation can miss short violations, the exact failure mode the paper uses to motivate continuous-time scoring.","Inference: the same arithmetic/geometric split could be applied to other quantitative semantics, for example robustness under parameter perturbations, yielding a score that is less brittle to noise; the paper does not explore this extension.","Inference: the numerical behavior of the geometric integral near zero scores is worth a dedicated test, since the logarithm in $\\ln(1+\\eta)$ or $\\ln(1-\\eta)$ could distort gradients when a subformula is close to its satisfaction boundary."],"forward_implications":["In falsification, minimizing AGIM instead of traditional robustness finds executions with more severe violations, because violations at every time and in every subformula contribute; the paper demonstrates this on an automatic transmission benchmark.","In control synthesis, maximizing AGIM makes agents enter assigned regions quickly and stay near their centers, because the time averages reward sustained satisfaction; the paper demonstrates this in two multi-agent examples.","The score is smooth almost everywhere and has non-zero gradient wherever it is smooth, making it compatible with gradient-based optimization for STL tasks.","Because sign agreement with traditional robustness holds, any AGIM-positive trajectory is guaranteed to satisfy the specification and any AGIM-negative trajectory is guaranteed to violate it, so the score can be used as a sound optimization objective.","AGIM distinguishes signals that the traditional score judges equally, such as two step responses with the same peak overshoot but very different overshoot durations."],"supporting_citations":[{"why":"Defines STL syntax and semantics over continuous-time signals, the object language the paper's score evaluates.","marker":"[5]"},{"why":"Supplies the traditional max/min robustness semantics whose sign the new AGIM score is required to agree with.","marker":"[9]"},{"why":"Provides a prior average-based robustness whose positive values do not imply satisfaction, the gap that AGIM's soundness result closes.","marker":"[18]"},{"why":"The authors' earlier discrete-time Arithmetic-Geometric Mean robustness, which AGIM extends to continuous-time signals.","marker":"[19]"},{"why":"Defines the geometric product integral used as the continuous analog of the product operator in the AGIM definitions.","marker":"[20]"},{"why":"Supplies the automotive falsification benchmark used in the case study comparing AGIM with traditional robustness.","marker":"[21]"}],"fun_headline_variants":["Average-based STL robustness uses entire signal, stays sound","Whole-signal averaging improves STL robustness and falsification","New STL robustness score averages over time, not just worst point","Sound STL robustness from averaging, more informative than min/max"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The recursive AGIM evaluation must decide an 'any' condition over a continuous interval, for example whether there exists a time in $[t+a,t+b]$ where the subformula score is non-positive, and in the implemented versions this is checked only on finitely many simulation samples, so very short violations between samples can be missed.","fun_headline_variants_meta":{"raw":{"variants":["Average-based STL robustness uses entire signal, stays sound","Whole-signal averaging improves STL robustness and falsification","New STL robustness score averages over time, not just worst point","Sound STL robustness from averaging, more informative than min/max"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000581,"raw_usage":{"total_tokens":2659,"prompt_tokens":790,"completion_tokens":1869,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":406,"completion_tokens_details":{"reasoning_tokens":1798}},"tokens_in":406,"tokens_out":1869,"duration_ms":143243,"temperature":1.0,"reasoning_tokens":1798,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:32:21.759748+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the AGIM algorithm on a continuous-time signal that contains a brief violation shorter than the implementation's sampling interval, such as a one-millisecond overshoot above the threshold in a step response sampled coarsely; if the sampled implementation returns a positive AGIM score for a Globally specification while the true continuous signal violates it, the practical soundness claim is falsified.","supporting_citations":[{"cited_title":"Robust control for signal temporal logic specifications using discrete average space robustness,","cited_arxiv_id":null,"evidence_quote":"Provides a prior average-based robustness whose positive values do not imply satisfaction, the gap that AGIM's soundness result closes."},{"cited_title":"Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications","cited_arxiv_id":"1903.05186","evidence_quote":"The authors' earlier discrete-time Arithmetic-Geometric Mean robustness, which AGIM extends to continuous-time signals."},{"cited_title":"Multiplicative calculus and its applications,","cited_arxiv_id":null,"evidence_quote":"Defines the geometric product integral used as the continuous analog of the product operator in the AGIM definitions."},{"cited_title":"Benchmarks for temporal logic requirements for automotive systems,","cited_arxiv_id":null,"evidence_quote":"Supplies the automotive falsification benchmark used in the case study comparing AGIM with traditional robustness."}],"review_version":1}