{"id":"ac5c5057-0543-4b64-a54d-d0cd1f44e30f","arxiv_id":"2509.01777","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"The paper formulates controller synthesis that maximizes the disturbance a closed-loop system can withstand under finite-horizon temporal logic specifications, with exact linear and probabilistic nonlinear solutions.","lead":"This paper defines a resilience metric for controlled dynamical systems: the largest disturbance a feedback controller can tolerate while still satisfying a temporal logic specification. It gives an exact reformulation for linear systems and a probabilistic scenario-based approach for nonlinear systems.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Linear 'exact' resilience values are only certified local optima of a nonconvex polynomial program; no global optimality check is provided.","rationale":"The reader's weakest-assumption analysis correctly identifies the most load-bearing issue: Theorem 1 is an equivalence to a nonconvex polynomial program, and the reported 'exact' resilience values are produced by a local solver without global optimality certificates. This is not merely a practical detail; it directly affects the paper's headline claim. If Ipopt returns a local maximum, then the computed controller is not necessarily maximally resilient, and the reported resilience understates or misstates the true value. The mathematical derivation via Farkas' lemma appears plausible, and I do not see an algebraic error in the reformulation itself; the gap is in the claim that exact solutions are 'provided' when the numerical pipeline does not certify global optimality. A single concrete check--re-solving the mobile-robot example with a certified global optimizer--would settle whether the reported 0.0686 is truly the global maximum. I agree with the reader's CONDITIONAL verdict: the issue is specific and addressable, not a fundamental invalidation of the framework, but it must be resolved before the exactness claim can be accepted. The scenario-optimization guarantee in Theorem 2 also relies on regularity properties of a nonconvex solver that are asserted rather than verified, but the linear exactness issue is the more central one.","tokens_in":12524,"tokens_out":20050,"duration_ms":255014,"concrete_test":"Re-solve the Theorem 1 mobile-robot instance from Section V.A (N=6, n=2, polytopic specification (13)) with a certified global polynomial optimizer, e.g., SCIP with spatial branching, BARON, or a rigorous branch-and-bound implementation, and compare the certified global optimum with Ipopt's reported 0.0686. If the verified optimum is strictly greater than 0.0686, the reported exact resilience is only a local lower bound and the exactness claim fails for the reported numbers. If the global solver cannot certify within the reported value, run the same comparison on a small analytically solvable linear instance to demonstrate whether Ipopt's local solutions match the true maximum.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The mathematical reformulation in Theorem 1 may be algebraically correct, but the central claim of 'exact solutions' is not substantiated for the reported numbers. Problem (4) is a nonconvex polynomial optimization: the variables α1, α2 appear nonlinearly inside A_bar = A + B α1, and P multiplies A_bar through the equality PA_b = E(α1). Equality to g_psi(x) in Theorem 1 means the global maximum of (4). The paper solves the case studies with Pyomo/Ipopt, a local interior-point solver, and provides no global optimality certificates, no dual bounds, and no multistart or branch-and-bound verification. Therefore the reported g_psi(x(0)) = 0.0686 in Section V.A, and similarly the ACC values in Table II for the scenario-based problem (10), are only upper/lower bounds? Specifically, for the linear case Ipopt can stop at a local maximum, making the computed resilience a lower bound on the true g_psi. Since the title and abstract promise 'maximally resilient controllers' and 'exact solutions', this is a load-bearing gap: the exactness of the computed value is exactly what the sharp satisfaction/violation transition in Figures 1-2 is used to demonstrate.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines a resilience metric for controlled discrete-time systems: the largest disturbance magnitude epsilon such that some parameterized feedback controller keeps all closed-loop trajectories within a finite-horizon temporal-logic specification psi. For linear dynamics with linear controllers and polytopic specifications, Theorem 1 reformulates the robust problem as a deterministic polynomial optimization via an affine Farkas lemma, and the paper calls this 'exact'. For nonlinear systems, nonlinear controllers, and general specifications including input constraints, the authors formulate a robust optimization and solve a scenario program (10), with a probabilistic satisfaction guarantee given in Theorem 2 using the non-convex scenario-optimization results of [21]. Two case studies, a mobile robot and an adaptive cruise control example, illustrate the approach.","tokens_in":12826,"tokens_out":13056,"duration_ms":140038,"significance":"The extension of temporal-logic resilience from uncontrolled systems [16] to controlled synthesis is a natural and valuable step. The Farkas-based reformulation in Theorem 1 is elegant and, if the global-optimality issue is handled, provides an exact characterization of resilience for a useful class of linear systems. The scenario-optimization route for nonlinear systems is practically relevant and gives a quantifiable, though approximate, guarantee. The mathematical derivation in the appendix appears sound at the symbolic level. The main caveat is that the numerical claims of 'exact' resilience values are not supported by the local NLP solver used, and the probabilistic theorem relies on a regularity assumption that is invoked but not verified in detail.","major_comments":[{"comment":"Theorem 1 equates g_psi(x) with the value of the polynomial optimization (4), and the abstract and case study claim 'exact' solutions, reporting g_psi(x(0))=0.0686. Problem (4) is nonconvex: alpha1 and alpha2 appear nonlinearly, and the equality P A_b = E(alpha1) is bilinear in P and polynomial in alpha. The numerical results are obtained with Pyomo/Ipopt, a local interior-point solver, and no global optimality certificates, dual bounds, or multistart/branch-and-bound verification are provided. A local solution is only a feasible point, so the computed value is a lower bound on the true global optimum and hence on the actual resilience. Consequently the 'sharp transition' claimed in Figures 1-2 does not demonstrate tightness of the reported threshold. Please either solve (4) to certified global optimality or explicitly reframe the numerical values as lower bounds while keeping Theorem 1","section":"Section V.A, Theorem 1/Eq. (4)"},{"comment":"The proof of Theorem 2 states that Property 1 of [21] is satisfied because a deterministic solver with consistent initialization is used. However, Property 1 is not stated in the manuscript, so the reader cannot verify this claim. For the nonconvex problem (10) solved by Ipopt, local solutions may be non-unique and dependent on initialization, and it is not obvious that repeatability is equivalent to the regularity condition required by [21]. Since Theorem 2 is the central guarantee for the nonlinear scenario approach, please state Property 1 explicitly and either prove it for problem (10) under the reported solver setup or state it as an explicit assumption. Without this, the probabilistic guarantee is not fully established.","section":"Appendix A-2, Theorem 2"}],"minor_comments":[{"comment":"There are numerical inconsistencies between the text and the figure captions. The text reports g_psi(x(0))=0.036 and 0.078 for the M=100 linear and polynomial ACC cases, while Figure 3 caption says 0.03 and Figure 4 caption says 0.045. Table II lists epsilon*_M=0.0367 for M=100. Please align these values.","section":"Section V, Figures 3-4"},{"comment":"The displayed definition of b(k) and t(k) is garbled; the summation limits and the equation for t(k) are not readable as printed. Please rewrite Equation (12) with standard notation so the dependence on beta and M is unambiguous.","section":"Section IV-B, Eq. (12)"},{"comment":"The statement says 'Suppose the set {x | Ex <= F} is not empty' before giving the Farkas equivalence. For the application in Section III, the nonempty set should be {Y | A_b Y <= B_b}; the conclusion Ex<=F for all such Y is what is being characterized. Please clarify which nonemptiness condition is intended, since the current wording is confusing.","section":"Appendix B, Theorem 3"},{"comment":"The sentence 'At four time steps, we observe that only few points fall outside the set B2, which confirms that... it is probabilistically guaranteed' conflates a finite-sample observation with the probabilistic bound. The guarantee in Theorem 2 is about the measure of violating disturbances, not about the displayed sample; please rephrase.","section":"Section V.B"},{"comment":"There are small typographical issues, e.g., 'takes 4s to converg' in Section V.B. The table formatting for the scenario results (Table II) is also hard to read; consider a clearer layout for alpha*1 and alpha*2.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The theoretical framework is a solid contribution, and the Farkas derivation is credible. The main risk is overclaiming 'exact' numerical results obtained with a local solver, and the unverified invocation of Property 1 in the probabilistic theorem. Both are fixable by careful revision: either certify global optimality (or temper the claims to lower bounds) and make the scenario-optimization assumptions explicit. I would not recommend rejection at this stage, but the current version should not be accepted without addressing these load-bearing points."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I skimmed arXiv:2509.01777. The one thing to know up front: the linear result is a genuine theoretical contribution, but 'exact' in the title and abstract is not earned by the numerical pipeline. The Farkas reformulation in Theorem 1 is a real step — it turns the robust constraint satisfaction problem into a polynomial optimization over the controller parameters and a multiplier matrix. That gives you a concrete object to maximize. The scenario extension for nonlinear systems is a sensible, competent application of Garatti–Campi nonconvex scenario theory.\n\nWhat the paper does well: the proof of Theorem 1 in the appendix is algebraically solid. The definition of controlled resilience (Definition 1) is a natural and useful generalization of the uncontrolled notion in [16]. The case studies illustrate the intended use, especially the ACC example where input constraints matter. The LTL_f connection is clean.\n\nThe soft spots are about the gap between what is proved and what is computed. Theorem 1 equates g_psi(x) with the global maximum of (4). Problem (4) is nonconvex — alpha1 enters nonlinearly through A+B alpha1 and multiplies P — and the authors solve it with Ipopt, a local interior-point solver. No global optimality certificates, no dual bounds, no multistart. So the reported g_psi(x(0)) = 0.0686 is at best a lower bound on the true resilience. Calling it 'exact' overstates what is actually certified. The same concern applies to the scenario results: nonconvex scenario theory (Theorem 2) needs a deterministic, measurable selection rule for the local optimum. The authors assert such a rule exists ('using a deterministic solver and consistent initialization') but they don't specify the initialization or the selection rule, and they never explain how s*_M support constraints were computed for these nonconvex problems. These are addressable issues, but they are not cosmetic.\n\nThere are also a few smaller blemishes: the Figure 3 caption says eps <= 0.03 while Table II gives 0.0367 for M=100; Figure 4 caption says 0.045 while the text reports 0.078 for the polynomial controller. A careful reader will trip on these.\n\nOverall, the theoretical framework holds up. The 'exact solutions' claim should be reworded to 'exact reformulation' with the numerical values presented as local optima unless certified globally. The paper deserves peer review; I'd send it back for revisions, asking for the supporting detail on the scenario solver and cleanup of the inconsistent numbers.","headline":"Good theory, overstated exactness: the Farkas reformulation is real, but the reported resilience values are only local optima unless globally certified.","tokens_in":13270,"tokens_out":6065,"would_cite":true,"duration_ms":63288,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C05","93C10","90C26"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper defines resilience as the largest disturbance a controlled system can absorb while still satisfying a temporal logic specification, and shows it can be computed exactly for linear systems and with probabilistic guarantees for non","keywords":["resilience metric","temporal logic specifications","controller synthesis","scenario optimization","Farkas lemma","robust optimization","linear systems","nonlinear systems"],"falsifier":"Take a scalar linear system x(k+1)=x(k)+u(k)+d(k) with a simple polytopic specification over a short horizon, compute the true resilience by brute-force search over epsilon and controller parameters, then solve the polynomial program (4) with a local solver; if the solver returns a strictly smaller value, the claim that the optimization computes the exact resilience is falsified for that instance.","tokens_in":12461,"feed_emoji":"🛡️","tokens_out":5857,"duration_ms":57908,"temperature":0.7,"pith_summary":"The paper defines the resilience of a controlled dynamical system as the largest disturbance level, measured in infinity norm, for which there exists a feedback controller such that all closed-loop trajectories satisfy a given finite-horizon temporal logic specification. The central claim is that for linear systems with linear controllers and polytopic specifications, this resilience value is exactly the optimum of a deterministic polynomial optimization problem, obtained by eliminating the universal quantifier over disturbance sequences with an affine Farkas lemma. For nonlinear systems, nonlinear controllers, and general specifications, the paper replaces the robust program by a scenario optimization and proves a probabilistic guarantee that the violation probability of the obtained controller is bounded by a computable quantity. If correct, the framework turns the question of how much disturbance a system can take into a concrete numerical value that can guide controller design.","feed_headline":"Solve for the largest disturbance a controller can survive","feed_subtitle":"Exact for linear systems, probabilistic for nonlinear ones, this metric quantifies a controller's resilience.","key_machinery":"The load-bearing object is the resilience metric g_psi(x), defined as a supremum over disturbance levels epsilon and controller parameters alpha. For linear systems, the clean conversion is done by the affine form of Farkas' lemma: it replaces the infinite set of constraints 'E(alpha1) Y <= (1/epsilon) F(...) for all Y with ||Y||_inf <= 1' by the existence of a nonnegative matrix P with P A_b = E(alpha1) and epsilon P B_b <= F(...). For nonlinear systems, the machinery is the scenario approach: sample i.i.d. disturbance sequences, solve a nonconvex program (10) that enforces the constraints on the samples only, and bound the generalization error via the support-constraints count s*_M and the","core_discovery":"The core discovery is Theorem 1: for a discrete-time linear system x(k+1)=Ax(k)+Bu(k)+d(k) with linear feedback u=alpha1 x+alpha2 and a specification written as products of polytopes, the resilience metric g_psi(x) equals the maximum of epsilon over alpha1, alpha2 and a nonnegative matrix P satisfying P>=0, P A_b = E(alpha1), and epsilon P B_b <= F(x,alpha1,alpha2), where A_b, B_b, E, F are explicitly constructed from the system matrices and the specification. This reduces a robust 'for all disturbance sequences' condition to a single polynomial program. For the nonlinear case, Theorem 2 states that the solution theta*_M of the scenario program (10) satisfies P^M( V(theta*_M) < b(s*_M) ) > 1","pith_inferences":["The exactness of the linear result hinges on global optimality of a nonconvex polynomial program; if a local solver is used, the reported resilience is a certified lower bound but not necessarily the maximum.","The scenario bound could likely be sharpened by using adaptive sampling or wait-and-judge schemes, since the paper's bound depends only on the number of support constraints.","The resilience metric could serve as an objective in contract-based or assume-guarantee synthesis, since it quantifies how much disturbance a controller can promise to tolerate.","A natural testable extension is to compare the scenario-optimized controller's realized violation frequency on a large out-of-sample set against the bound b(s*_M)."],"forward_implications":["For linear systems with linear controllers and polytopic specifications, resilience and the maximizing controller can be obtained from one polynomial optimization program rather than a search over disturbance sequences.","Nonlinear control designs inherit a probabilistic certificate: with a chosen confidence, the probability that a new i.i.d. disturbance violates the specification is bounded by b(s*_M).","The same formulation covers finite-horizon safety, exact-time reachability, and convex linear temporal logic over finite traces within one framework.","Adding input constraints is straightforward in the scenario approach, at the cost of exactness.","The resilience value gives an operational meaning to safety margin: the largest infinity-norm disturbance level the closed loop tolerates while meeting its specification."],"supporting_citations":[{"why":"Introduces the resilience metric for non-controlled systems, which this paper extends to controlled systems with controller synthesis.","marker":"[16]"},{"why":"Provides the affine form of Farkas' lemma used to convert the robust disturbance constraints into matrix inequalities in Theorem 1.","marker":"[20]"},{"why":"Supplies the non-convex scenario optimization theory and Theorem 6 that underpins the probabilistic guarantee of Theorem 2.","marker":"[21]"},{"why":"Defines the complexity s*_M and the risk bound b(k) used in the scenario guarantee.","marker":"[22]"}],"fun_headline_variants":["Maximize disturbance tolerance in temporal logic control","Biggest disturbance a controller can take under specs","Max resilience for controllers under temporal logic","Tuning control to survive the biggest disturbance","Max disturbance a controller can withstand"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The exactness claim for linear systems assumes the nonconvex polynomial optimization in Theorem 1 is solved to global optimality; the paper does not provide such a certificate and uses a local solver in the case studies, so the reported resilience values are only guaranteed to be lower bounds.","fun_headline_variants_meta":{"raw":{"variants":["Maximize disturbance tolerance in temporal logic control","Biggest disturbance a controller can take under specs","Max resilience for controllers under temporal logic","Tuning control to survive the biggest disturbance","Max disturbance a controller can withstand"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000441,"raw_usage":{"total_tokens":2049,"prompt_tokens":696,"completion_tokens":1353,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":440,"completion_tokens_details":{"reasoning_tokens":1299}},"tokens_in":440,"tokens_out":1353,"duration_ms":11490,"temperature":1.0,"reasoning_tokens":1299,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T12:11:23.122038+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a scalar linear system x(k+1)=x(k)+u(k)+d(k) with a simple polytopic specification over a short horizon, compute the true resilience by brute-force search over epsilon and controller parameters, then solve the polynomial program (4) with a local solver; if the solver returns a strictly smaller value, the claim that the optimization computes the exact resilience is falsified for that instance.","supporting_citations":[{"cited_title":"Temporal Logic Resilience for Dynamical Systems","cited_arxiv_id":"2404.19223","evidence_quote":"Introduces the resilience metric for non-controlled systems, which this paper extends to controlled systems with controller synthesis."},{"cited_title":"Schrijver,Theory of linear and integer programming, ser","cited_arxiv_id":null,"evidence_quote":"Provides the affine form of Farkas' lemma used to convert the robust disturbance constraints into matrix inequalities in Theorem 1."},{"cited_title":"Non-convex scenario optimization,","cited_arxiv_id":null,"evidence_quote":"Supplies the non-convex scenario optimization theory and Theorem 6 that underpins the probabilistic guarantee of Theorem 2."},{"cited_title":"Risk and complexity in scenario optimization,","cited_arxiv_id":null,"evidence_quote":"Defines the complexity s*_M and the risk bound b(k) used in the scenario guarantee."}],"review_version":1}