{"id":"e5774506-d0d1-4627-8b3d-6fb8c5b67ea7","arxiv_id":"2507.12339","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Given a discrete-time system and its symbolic abstraction, the paper computes the largest additive disturbance that preserves the alternating simulation relation, with uniform and non-uniform versions and a tightness bound tied to reachable-set error.","lead":"Symbolic control approximates a continuous system by a finite model; this paper shows that such a model already tolerates small extra disturbances without being rebuilt. It provides formulas for the exact maximum disturbance, state by state and input by input, and proves the bound is tight when the reachable-set approximation is accurate.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Tightness half of Theorem 3.2 depends on an unproved witness z in Eq. (8); compactness or upper hemicontinuity of the over-approximation is missing, so the margin is not shown tight as stated.","rationale":"I read the paper in good faith: the main contribution is the explicit robustness margin eta and the sufficiency theorem showing that any additive disturbance below eta preserves the alternating simulation relation. That direction is essentially correct, modulo standard technical assumptions about compactness of reachable sets and the usual epsilon0 < eta argument. The reader's weakest assumption targets the tightness direction, and I agree that is the most load-bearing insecure step. The proof of the third item of Theorem 3.2 needs a witness z in q at which the margin is realized, but Eq. (3) only defines a supremum over the cell. The paper does not supply the compactness/upper hemicontinuity hypotheses that would justify the minimizer/witness argument. This is not an attack on the authors; it is a missing hypothesis in an otherwise plausible theorem. Because the sufficiency direction and the controller refinement proposition do not rely on this witness step, the central positive claim survives, but the advertised tightness of the margin and the delta-overapproximation discussion are conditional on a proof gap. The reader's CONDITIONAL verdict remains appropriate; no stronger action is needed if the authors add the missing regularity assumptions and prove Eq. (8) rigorously. I am not pressing the possible one-sided reading of the delta-overapproximation definition because it is likely a typographical issue; the witness/compactness gap is independent and decisive.","tokens_in":14105,"tokens_out":25457,"duration_ms":329473,"concrete_test":"Formalize the step from Eq. (3) to Eq. (8) under the stated hypotheses of Theorem 3.2. Concretely, define a two-cell example with q=[0,infinity) and a closed, noncompact over-approximation K = bar f(q,u,D) contained in Int(Q^{-1}(Delta_d(q,u))) whose distance to the boundary of Q^{-1}(Delta_d(q,u)) is 0, and check whether Eq. (8) has a witness z in q. If no witness exists, or if the derivation requires adding compactness and upper hemicontinuity of bar f, then Theorem 3.2 item 3 is incomplete as stated; otherwise the reader's concern is settled.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing weak point is the negative (tightness) half of Theorem 3.2, item 3. The proof needs Eq. (8): a point z in q such that for every epsilon0 > epsilon(z,u), cl(bar f(z,u,D)) + B_{epsilon0}(0) leaves Q^{-1}(Delta_d(q,u)). This is asserted from the definition of eta in Eq. (3), but Eq. (3) is a supremum over the whole cell q: it produces a point of the expanded reachable set of the cell, not a point belonging to the fiber of a single z in q. Extracting z requires compactness of bar f(q,u,D) and upper hemicontinuity of x -> bar f(x,u,D), or an explicit infimum-over-x definition of the margin. The paper assumes only that bar f(q,v,D) is closed, and X is not assumed bounded; q may be unbounded. Without these hypotheses Eq. (8) can fail even when the over-approximation is closed and the margin is approached only in the limit. The sufficiency direction (mu < epsilon implies alternating simulation) does not depend on this witness step and appears sound, but the advertised tightness, including the delta-overapproximation discussion and the claim that exact reachable sets give tight margins, is not established by the proof as written.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a notion of robustness margin for symbolic models of discrete-time control systems. Given an abstraction S_d(Σ) of a disturbance-free system, it defines a state- and input-dependent quantity η from the over-approximated reachable set and the successor cells, and proves (Theorem 3.2) that if an additive disturbance μ is pointwise below this margin, the same alternating simulation relation still holds between the abstraction and the perturbed system; it further claims a tightness result up to the reachability error δ, derives a uniform margin (Corollary 3.3), and applies the margin to controller refinement (Proposition 3.4). Two examples illustrate the computation and use of the margins.","tokens_in":14361,"tokens_out":14565,"duration_ms":176198,"significance":"The conceptual contribution is attractive: if the main theorem is correct, a precomputed symbolic model carries a quantitative guarantee on how much disturbance it can tolerate, and controllers synthesized for the disturbance-free abstraction can be reused for all perturbed systems below the margin. The sufficiency direction of Theorem 3.2 and the controller-refinement proposition are clean and appear sound; the paper also gives concrete algorithmic recipes and two worked examples, which help communicate the idea. However, the advertised tightness results depend on several hypotheses that are either missing or not stated precisely: without them, the negative half of Theorem 3.2 and the uniform-margin corollary are not established. I regard the paper as a promising contribution whose central claims need a substantial proof repair rather than a rejection.","major_comments":[{"comment":"The proof infers from cl(\\bar f(q,u,D)) ⊆ Int(Q^{-1}(Δ_d(q,u))) that there exists α>0 with cl(\\bar f(q,u,D))+B_α(0) ⊆ Int(Q^{-1}(Δ_d(q,u))). This inference is not valid without compactness of cl(\\bar f(q,u,D)) or a positive-distance condition: a closed noncompact set can lie inside an open set while having distance zero to its complement (for example, a graph approaching the boundary at infinity). The paper does not assume X bounded or \\bar f(q,u,D) compact, so the claimed ε(x,u)>0, and the positivity part of Corollary 3.3, are not established as stated. Adding an assumption that cl(\\bar f(q,u,D)) is compact, or defining the margin with an explicit positive-distance condition, would repair this step.","section":"Section 3.1, proof of Theorem 3.2, first item"},{"comment":"The existence of a single z∈q satisfying Eq. (8) for every ε0>ε(z,u) is asserted without proof. The margin η(q,u,A) in Eq. (3) is a supremum taken over the cell-level over-approximated reachable set \\bar f(q,u,D); it does not by itself provide a point z whose pointwise reachable set attains that supremum. Extracting such a z requires compactness of cl(\\bar f(q,u,D)) and upper hemicontinuity of x↦\\bar f(x,u,D), or an explicit infimum-over-x definition of the margin, none of which is stated. Absent this, the tightness claim in item 3, and the analogous claim in Eq. (11) of Corollary 3.3, are not established; the sufficiency half of the theorem is unaffected.","section":"Section 3.1, Theorem 3.2, item 3, Eq. (8)"},{"comment":"The proof uses the equality cl(\\bar f(z,u,D)) = \\bar f(z,u,D) after selecting z∈q. The closedness hypothesis in the theorem concerns cell-level sets \\bar f(q,v,D) for q∈X_d, v∈U_d, not the pointwise sets \\bar f(z,u,D) for continuous states z. Unless \\bar f(q,v,D) is defined as the union of pointwise images and pointwise closedness is assumed, this equality is unjustified. The same issue appears in Corollary 3.3.","section":"Section 3.1, proof of Theorem 3.2, third item"},{"comment":"The δ-overapproximation condition should be stated with a clear inclusion direction. As printed, footnote 1 appears to read f(x,u,D) ⊆ \\bar f(x,u,D)+B_δ(0), whereas the proof needs the opposite inclusion, \\bar f(z,u,D) ⊆ f(z,u,D)+B_δ(0), to justify \\bar f(z,u,D)+B_{μ-δ}(0) ⊆ f(z,u,D)+B_μ(0). If the intended definition is \\bar f(x,u,D) ⊆ f(x,u,D)+B_δ(0), it should be stated explicitly and the term 'overapproximation' clarified, since many standard reachable-set overapproximations are only guaranteed to satisfy the forward inclusion f ⊆ \\bar f+B_δ unless a two-sided error bound is imposed.","section":"Section 3.1, footnote 1 and proof of the third item"}],"minor_comments":[{"comment":"The sentence 'To show that R in (10) is not an alternating simulation relation' should refer to Eq. (5), not Eq. (10), which belongs to Corollary 3.3.","section":"Section 3.1, proof of Theorem 3.2"},{"comment":"The Argmax operation in Eq. (13) returns a set, so the expression defines a set-valued map rather than a deterministic controller; a tie-breaking rule or a choice function should be specified.","section":"Section 3.4, Eq. (13)"},{"comment":"The overline distinguishing \\bar f from f is frequently lost in the typeset equations, which makes the direction of the δ-overapproximation assumption difficult to verify; using a distinct symbol for the overapproximated reachable map would improve readability.","section":"Throughout"},{"comment":"There are several typos: 'there exits' should be 'there exists' in the proof of Theorem 3.2, '𝑞∈𝑋𝑞' should presumably be '𝑞∈𝑋𝑑', and 'Σ̄ 𝜇' in Corollary 3.3 should be 'Σ_𝜇'.","section":"Throughout"},{"comment":"The row for N_u=3 shows the uniform margin staying constant at 0.0237 for N_x=1600, 3200, and 6400 before dropping at 12800; a brief explanation of this plateau would help the reader interpret the trade-off between discretization and robustness.","section":"Section 4.1, Table 1"}],"recommendation":"major_revision","confidential_remarks":"The sufficiency direction and the controller refinement result are the strongest parts of the paper and appear sound. The advertised tightness results, which form a central part of the contribution, currently rely on missing compactness/continuity hypotheses, an unjustified pointwise closedness step, and an unclear δ-overapproximation inclusion direction. These are repairable within the scope of the paper by adding explicit hypotheses and clarifying the definition, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe paper is worth your time if you work on abstraction-based control: it makes explicit a robustness margin that is implicit in every symbolic abstraction. The sufficiency result (Theorem 3.2, item 2) is correct and clean: if the additive disturbance μ(x,u) is pointwise below η(Q(x),u,Δ_d(Q(x),u)), the relation {(x,q): x∈q} remains an alternating simulation from the abstraction to the perturbed system. That gives a direct way to reuse a disturbance-free abstraction and controller for a whole family of perturbed systems. The uniform-margin corollary and the controller-refinement proposition are straightforward and useful. The observation that tightness of the margin tracks the tightness of the reachable-set over-approximation is also correct in spirit.\n\nThe weak point is the tightness half (Theorem 3.2, item 3). The proof needs a z∈q that witnesses the margin in the sense of Eq. (8): a single point whose expanded reachable fiber leaves the target for every ε above the local margin. But η is defined as a supremum over the whole cell's over-approximated reachable set. The supremum yields a point of that cell-level set, not a point belonging to the fiber of a specific z. Extracting such a z requires compactness of \\bar f(q,u,D) and some upper hemicontinuity of x↦\\bar f(x,u,D), or an explicit infimum-over-x definition of the margin. The paper assumes only that \\bar f(q,u,D) is closed, which is not enough. The sufficiency direction does not depend on this step, and the example in Fig. 4 shows the expected behavior, but the formal tightness claim, and the δ=0 'tightness' remark, are not established by the proof as written.\n\nThe examples are purely illustrative; no code or data is shipped, so the practical gain is asserted rather than demonstrated. The notation in the δ-overapproximation part of the proof is also under-specified, which makes the tightness argument harder to check.\n\nOn novelty: the sufficiency half is close to what some of us would call folklore, but the state/input-dependent margin and the explicit tightness analysis are a real extension of [11]. The paper is honest about its limitations and the literature is cited appropriately.\n\nWho should read it: people working on symbolic controller synthesis who need robustness guarantees. The paper deserves a serious referee, but the tightness proof needs a missing hypothesis or a redefinition of η before publication. I would send it to review with a request for revision, not desk-reject it. I would bring it to a reading group, and I would cite it — but only the sufficiency half until the gap is closed.","headline":"A well-motivated robustness margin for symbolic abstractions; sufficiency is solid, but the tightness proof has a gap that needs a fix before publication.","tokens_in":14877,"tokens_out":5802,"would_cite":true,"duration_ms":63849,"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":"The paper proves that every symbolic abstraction carries a built-in robustness margin, so the same finite model remains a valid contract for any perturbed system whose disturbance stays below that margin.","keywords":["robust control","symbolic control","robustness margin","alternating simulation relation","reachability analysis","abstraction-based controller synthesis","perturbed discrete-time systems","temporal logic specifications"],"falsifier":"Pick a cell $q$ and input $u$ in the paper's double-integrator example (exact reachable sets, $\\delta=0$, uniform margin $0.01125$), locate a point $z\\in q$ at which the local margin attains its minimum, and apply a constant disturbance of magnitude $\\varepsilon(z,u)+0.001$. If the one-step successor never leaves the union of symbolic successor cells, the tightness assertion of Theorem 3.2 is false; if it lands outside, tightness is confirmed on that instance.","tokens_in":13895,"feed_emoji":"🛡️","tokens_out":12613,"duration_ms":127480,"temperature":0.7,"pith_summary":"Given a discrete-time control system and a finite symbolic abstraction built from reachable-set over-approximations, the paper proves that the abstraction is not only a model of the disturbance-free system: it is also a valid model of every perturbed version whose additive disturbance, at each state and input, is smaller than a margin that can be read off from the abstraction's geometry. The margin is strictly positive everywhere, so this robustness is free -- it comes from the slack between the over-approximated reachable set and the boundary of the set of symbolic successors. The paper gives a constructive formula for the margin, a uniform version valid for all states and inputs, and a tightness result: when reachable sets are computed exactly, any disturbance larger than the margin breaks the behavioral relation, and with a $\\delta$-over-approximation the breaking threshold is the margin plus $\\delta$. It then shows how a controller synthesized for the disturbance-free abstraction refines to the perturbed system, and how to choose among admissible inputs the one maximizing the margin.","feed_headline":"Symbolic models tolerate disturbances up to a computable margin","feed_subtitle":"An abstraction built for the disturbance-free system still controls every perturbed version within the margin.","key_machinery":"The load-bearing object is the robustness-margin map $\\eta(q,v,A)$, defined as the supremum radius by which the over-approximated reachable set $\\mathrm{cl}(\\bar f(q,v,D))$ can be inflated while remaining inside the interior of $Q^{-1}(A)$, the union of cells that are symbolic successors. Lemma 3.1 shows this radius is always positive: because a symbolic transition exists exactly when the over-approximated reachable set touches the closure of the successor cell, the set must actually lie strictly inside the interior of the union of successors. Theorem 3.2 converts that geometric slack into an admissible disturbance level, and the $\\delta$-over-approximation gap into the tightness error. The same slack appears as the uniform margin $\\min_{q,v}\\eta(q,v,\\Delta_d(q,v))$ in Corollary 3.3.","core_discovery":"Let $S_d(\\Sigma)$ be the symbolic model whose transitions come from an over-approximation $\\bar f$ of the reachable set, and let $\\eta(q,v,A)$ be the largest radius $\\varepsilon$ such that the inflated reachable set $\\mathrm{cl}(\\bar f(q,v,D)) + \\mathcal{B}_{\\varepsilon}(0)$ stays inside the interior of $Q^{-1}(A)$. The paper's central claim is that the relation $\\{(x,q): x\\in q\\}$ is an alternating simulation relation from $S_d(\\Sigma)$ to the perturbed system $S(\\Sigma_\\mu)$ whenever $\\mu(x,u) < \\eta(Q(x),u,\\Delta_d(Q(x),u))$ for all state-input pairs. Conversely, when $\\bar f$ is a $\\delta$-over-approximation with closed values, if $\\mu(x,u) > \\eta(Q(x),u,\\Delta_d(Q(x),u)) + \\delta$ for some pair, the relation is not an alternating simulation relation. The margin is therefore both a certificate of robustness and, up to the over-approximation error $\\delta$, the largest disturbance the abstraction can tolerate; with exact reachable sets the margin is tight.","pith_inferences":["The margin could be monitored online: compare the current disturbance estimate against $\\varepsilon(x,u)$ and recompute the abstraction only when the margin is violated, rather than over-approximating disturbances a priori.","Because the uniform margin is a minimum over finitely many cells, it will often be dominated by the tightest transition; the same machinery could be applied locally, cell by cell, to avoid wasting reachability effort on transitions with large slack.","The geometric argument is not tied to alternating simulation specifically -- analogous slack in any abstraction relation (for instance feedback refinement or approximate simulation) should yield a similar free disturbance margin.","A specification-aware version that computes the margin for the predecessor operator rather than the full successor set would likely give larger effective margins for safety and reachability tasks."],"forward_implications":["Any controller synthesized on the disturbance-free symbolic model remains correct for the perturbed system under the same specification, provided $\\mu(x,u)<\\varepsilon(x,u)$ at every step.","The uniform margin $\\varepsilon = \\min_{q,v}\\eta(q,v,\\Delta_d(q,v))$ is strictly positive and protects all states and inputs simultaneously, so no per-state disturbance measurement is needed.","If reachable sets are computed exactly, the margin is tight: adding any disturbance above the margin destroys the alternating simulation relation.","With a $\\delta$-over-approximation of reachable sets, the threshold shifts by $\\delta$, so improving reachability tightness directly enlarges the guaranteed robustness.","Finer discretization of the state and input spaces reduces the uniform margin, making the known trade-off between abstraction accuracy and disturbance tolerance explicit."],"supporting_citations":[{"why":"Supplies the transition-system formalism, the alternating-simulation definition, and the standard symbolic-model construction the paper starts from.","marker":"[18]"},{"why":"Introduces feedback refinement relations and the growth-bounds reachability technique used for the mobile-robot abstraction.","marker":"[13]"},{"why":"The earlier robustness-margin approach for finite abstractions that this paper extends to maximal admissible disturbance margins.","marker":"[11]"},{"why":"Provides the set-propagation reachability methods used to compute the exact reachable sets whose slack defines the margin in the double-integrator example.","marker":"[1]"},{"why":"Supplies the delta-over-approximation results for linear reachability that the tightness argument invokes when delta is positive.","marker":"[10]"},{"why":"Supplies the corresponding delta-over-approximation results for nonlinear reachability used in the general tightness statement.","marker":"[15]"},{"why":"Establishes that symbolic models with alternating simulation exist for general nonlinear control systems, the setting in which the margin is defined.","marker":"[20]"},{"why":"Provides the algorithmic controller-synthesis machinery for temporal-logic specifications whose correctness the refinement result preserves.","marker":"[6]"}],"fun_headline_variants":["Free robustness margins in symbolic control","Computable margins protect perturbed symbolic systems","Symbolic models tolerate disturbances up to a limit","Robustness margin computed for symbolic control","Maximum disturbance for symbolic control now computable"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The tightness half of the main theorem relies on the assumption that the over-approximated reachable set is closed and bounded enough for the worst-case point inside a cell to exist; if that assumption fails, the sufficiency direction still holds but the claim that exceeding the margin destroys the simulation relation is not established.","fun_headline_variants_meta":{"raw":{"variants":["Free robustness margins in symbolic control","Computable margins protect perturbed symbolic systems","Symbolic models tolerate disturbances up to a limit","Robustness margin computed for symbolic control","Maximum disturbance for symbolic control now computable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00024,"raw_usage":{"total_tokens":1507,"prompt_tokens":923,"completion_tokens":584,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":539,"completion_tokens_details":{"reasoning_tokens":519}},"tokens_in":539,"tokens_out":584,"duration_ms":6832,"temperature":1.0,"reasoning_tokens":519,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T16:51:11.934863+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Pick a cell $q$ and input $u$ in the paper's double-integrator example (exact reachable sets, $\\delta=0$, uniform margin $0.01125$), locate a point $z\\in q$ at which the local margin attains its minimum, and apply a constant disturbance of magnitude $\\varepsilon(z,u)+0.001$. If the one-step successor never leaves the union of symbolic successor cells, the tightness assertion of Theorem 3.2 is false; if it lands outside, tightness is confirmed on that instance.","supporting_citations":[{"cited_title":"Verification and control of hybrid systems: a symbolic approach","cited_arxiv_id":null,"evidence_quote":"Supplies the transition-system formalism, the alternating-simulation definition, and the standard symbolic-model construction the paper starts from."},{"cited_title":"Feedback refinement relationsforthesynthesisofsymboliccontrollers","cited_arxiv_id":null,"evidence_quote":"Introduces feedback refinement relations and the growth-bounds reachability technique used for the mobile-robot abstraction."},{"cited_title":"Nonlinear Analysis: Hybrid Systems 22, 1–15","cited_arxiv_id":null,"evidence_quote":"The earlier robustness-margin approach for finite abstractions that this paper extends to maximal admissible disturbance margins."},{"cited_title":"Setpropagationtechniques for reachability analysis","cited_arxiv_id":null,"evidence_quote":"Provides the set-propagation reachability methods used to compute the exact reachable sets whose slack defines the margin in the double-integrator example."},{"cited_title":"Reachability analysis of linear systemsusingsupportfunctions.NonlinearAnalysis:HybridSystems 4, 250–262","cited_arxiv_id":null,"evidence_quote":"Supplies the delta-over-approximation results for linear reachability that the tightness argument invokes when delta is positive."},{"cited_title":"Accurate reachability analysis of uncertainnonlinearsystems,in:Proceedingsofthe21stinternational conferenceonhybridsystems:Computationandcontrol(partofCPS week), pp","cited_arxiv_id":null,"evidence_quote":"Supplies the corresponding delta-over-approximation results for nonlinear reachability used in the general tightness statement."},{"cited_title":"Symbolicmodels for nonlinear control systems without stability assumptions","cited_arxiv_id":null,"evidence_quote":"Establishes that symbolic models with alternating simulation exist for general nonlinear control systems, the setting in which the margin is defined."},{"cited_title":"volume 89","cited_arxiv_id":null,"evidence_quote":"Provides the algorithmic controller-synthesis machinery for temporal-logic specifications whose correctness the refinement result preserves."}],"review_version":1}