{"id":"f692057c-93be-48ef-b871-c41193c703c7","arxiv_id":"1908.03980","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Barrier-function-based sufficient conditions are derived for forward pre-invariance, invariance, pre-contractivity, and contractivity of closed sets in hybrid inclusions.","lead":"This paper derives mathematical tests, based on barrier functions, that certify when solutions of a hybrid system remain inside a prescribed set and, from the boundary, move toward its interior. The tests target hybrid inclusions, a general model that allows nonunique solutions and solutions that stop early, which previous barrier-function results did not handle.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's proof applies the one-sided Lipschitz condition (21) to a projection y1 that may lie outside ∂(K∩C), so the boundary-only invariance result is not established as stated.","rationale":"The reader's conditional verdict is appropriate, and the weakest assumption identified is exactly the load-bearing concern. I traced the proof of Theorem 2 and confirmed that condition (21) is quantified over y∈∂(K∩C), while the proof applies it to y1, the projection onto Ke, which the proof itself allows to lie outside C. Consequently, the one-sided Lipschitz inequality is not available at that point, and the uniqueness-function argument for δ1 collapses. This directly affects the central new contribution of the paper: the boundary-only sufficient conditions for forward pre-invariance. The paper's other results, especially Theorem 1 and the contractivity theorems, appear more standard and are not undermined by this specific gap. The self-reference to [41] for several proofs is a secondary but real obstacle to verification. I therefore see no reason to move beyond the reader's CONDITIONAL verdict; the required change is a repaired proof or a strengthened hypothesis in Theorem 2, not a rejection of the paper's broader framework.","tokens_in":35713,"tokens_out":8542,"duration_ms":94082,"concrete_test":"Independently re-derive the step from (26) to (27) in the proof of Theorem 2 using y2 in place of y1 whenever (21) is invoked, and check whether case (a) still yields the required inequality without assuming (21) at y1. If the derivation fails, extend Theorem 2's hypothesis (21) to all y∈∂Ke (or restrict y1 to ∂(K∩C)) and record whether the theorem remains true. As a numerical check, instantiate the geometry of Example 6 with a smooth F satisfying (21) on ∂(K∩C) with ρ(ω)=ω logω and with condition (a) enforced on (∂Ke)\\C; simulate the trajectory starting at the origin to see whether it leaves K. A positive escape would show the stated hypotheses are insufficient.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing gap is in the proof of Theorem 2. Condition (21) is assumed only for y∈∂(K∩C). In the proof, after defining y1 as the projection of x(t,0) onto Ke and y2 as the projection onto K∩C, the text explicitly allows y1 to lie in (U(∂Ke∩∂C)∩∂Ke)\\C, i.e., outside C and hence outside ∂(K∩C). Nevertheless, the proof then applies (21) with y=y1 to pass from (26) to (27) and invoke the uniqueness function. For such y1, (21) is not available, and F(y1) is not covered by the regularity assumptions stated on C. Thus the differential inequality for δ1 is unsupported. Since Theorem 2 is advertised as the main relaxation of Theorem 1, allowing boundary-only flow checks, this is not a cosmetic issue: either the proof must be repaired, or (21) must be strengthened to include projections onto Ke, or an additional argument must show y1∈∂(K∩C) under case (a). A secondary issue is that several proofs are deferred to reference [41], which is this same preprint, so the gap cannot be resolved by consulting the cited source.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies sufficient conditions for forward pre-invariance and pre-contractivity of closed sets for hybrid inclusions modeled as in (1). The set of interest is described by the intersection of zero-sublevel sets of a vector-valued barrier function candidate, and the results give infinitesimal conditions on the flow and jump maps that avoid computing solutions. Several variants are presented: C^1 barrier functions (Theorem 1), boundary-only flow checks under a one-sided Lipschitz condition on the flow map (Theorem 2), cone-based conditions (Theorem 3), locally Lipschitz barrier functions (Theorems 4 and 6), relaxed flow conditions using uniqueness functions (Proposition 1), and contractivity results for general closed sets and for C-sets. Examples include a thermostat, a bouncing ball, and a two-dimensional nonconvex example.","tokens_in":35990,"tokens_out":11224,"duration_ms":98111,"significance":"If the results hold, the paper extends barrier-function certificates from differential equations and hybrid automata to the broader setting of hybrid inclusions, addressing the complications of nonunique solutions and solutions that terminate prematurely. The explicit treatment of multiple barrier functions and the use of uniqueness functions to relax the flow inequalities are potentially valuable for safety verification in hybrid systems. The examples are illustrative and the overall structure is mostly careful. However, the main boundary-only relaxation, Theorem 2, currently contains a derivation gap that affects the advertised relaxation of Theorem 1, so the significance is conditional on repairing that gap.","major_comments":[{"comment":"The proof applies the one-sided Lipschitz condition (21) to the point y1, defined as a projection of x(t,0) onto Ke. The text explicitly allows y1 to lie in (U(∂Ke∩∂C)∩∂Ke)\\C, i.e., outside C. Since condition (21) is assumed only for y∈∂(K∩C), and y1∉C implies y1∉K∩C, the inequality used to pass from (26) to (27) is not available for such y1. This is a genuine derivation gap in the advertised boundary-only relaxation of Theorem 1. The proof must be repaired, for example by strengthening (21) to hold for all y∈Ke in the relevant neighborhood, or by providing a separate argument for the case y1∉C.","section":"Section 3.2, Theorem 2 (proof, conditions (21), (26), (27))"}],"minor_comments":[{"comment":"Several statements contain the sentence 'The proof is in [41]' where [41] is the same arXiv preprint; the proofs actually appear in the manuscript, so these sentences should be deleted or corrected to avoid a circular-reference appearance.","section":"Throughout (e.g., before Theorem 4, Proposition 2, Lemma 1, Theorem 6)"},{"comment":"References [27] and [29] are the same conference paper; they should be merged or renumbered to avoid duplication.","section":"References"},{"comment":"The definition of G(x) is written as 'G(x) :=[0,x 2]× [0,|x1|]', which appears malformed; it should be a set such as {0}×[0,|x_1|] or equivalent.","section":"Example 1"},{"comment":"Condition (41) is stated as 'for each i ={1,2,...,m}' instead of 'for each i∈{1,2,...,m}'.","section":"Theorem 5"},{"comment":"There are several typos, e.g., 'there exits' instead of 'there exists' in multiple places, and 'different forward invariance' in the abstract should be 'different forward invariance'.","section":"Throughout"},{"comment":"The projections y1 and y2 are not necessarily unique unless the sets are convex; the argument should clarify that any projection possessing the stated properties is selected, since the distance equality |x−y_i| = |x|_Ke or |x|_K∩C holds for any projection.","section":"Proof of Theorem 2"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid contribution in scope, but the proof of Theorem 2 as written does not support the boundary-only relaxation claim. The gap is specific and likely repairable, but it is load-bearing for one of the paper's advertised new results. The repeated 'The proof is in [41]' references to the same preprint, although accompanied by actual proofs, are unprofessional and should be cleaned up."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, it is a real and mostly careful extension of barrier-function tools to hybrid inclusions, with multiple barriers and a uniqueness-function relaxation that are genuinely new. Second, the proof of Theorem 2, the advertised boundary-only result, has a gap that needs repair before the theorem is trustworthy. I also found it annoying that several proofs are punted to reference [41], which is this same preprint.\n\nThe good parts are substantial. Theorem 1 gives clean infinitesimal flow and jump conditions for forward pre-invariance using multiple C^1 barriers, avoiding the single-scalar-function assumption common in the literature. Proposition 1 relaxes the flow inequality using uniqueness functions in a way I have not seen before for hybrid inclusions, and the examples—thermostat, bouncing ball, the non-convex flow set in Example 6—are illustrative and honestly discussed. The contractivity section extends the known C-set/Minkowski-functional approach to general closed sets and gives barrier-based sufficient conditions that look right. Most of the proofs I checked are carefully constructed, especially Lemma 3 and the cone-characterization lemmas.\n\nThe soft spot is Theorem 2. The idea is to replace the neighborhood flow condition by a one-sided Lipschitz-like condition (21) plus boundary/Lyapunov-type checks. In the proof, the projection y1 used under case (a) can land on (U(∂Ke∩∂C)∩∂Ke)\\C, i.e., on the boundary of C but outside C. That point is still in ∂(K∩C), so the stress-test's claim that it lies outside ∂(K∩C) is not correct. But the real problem is that F(y1) appears in the right-hand side of (21), and F is only assumed to be defined on C. If y1∉C, F(y1) may not exist, and the inclusion (21) is meaningless. The proof applies (21) with y=y1 anyway, so the differential inequality for δ1 is unsupported. This is fixable—for example, by assuming F is defined on a neighborhood of C, or by strengthening the projection argument to show y1∈C under the hypotheses—but it is not a cosmetic issue.\n\nSecondary issue: Theorem 4, Lemma 1, Proposition 2, and Theorem 6 all say “proof in [41],” and [41] is the arXiv version of this same paper. That is circular as a submission practice and should not be accepted in peer review.\n\nWho this is for: people working on safety and invariance for hybrid systems, especially control barrier functions for switched or impulsive dynamics. It deserves a serious referee, not a desk reject, but the review should ask for a repaired Theorem 2 and complete proofs in the manuscript.","headline":"Solid extension of barrier-function certificates to hybrid inclusions, but the proof of the boundary-only invariance theorem has a gap in the domain of the flow map, and several proofs are deferred to the same arXiv preprint.","tokens_in":36432,"tokens_out":3883,"would_cite":true,"duration_ms":38818,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C30","93D30","34A60","93B03"],"pacs":[],"model":"deepseek-v4-flash","headline":"By checking infinitesimal inequalities near the boundary of each constraint, a vector-valued barrier function can certify that a closed set is forward pre-invariant or pre-contractive for a hybrid inclusion, without computing any solution.","keywords":["barrier functions","forward invariance","contractivity","hybrid inclusions","hybrid systems","safety verification","uniqueness functions","set invariance"],"falsifier":"Consider the differential inclusion with $C=\\mathbb{R}^2$, $D=\\emptyset$, $F(x)=\\{[1,\\sqrt{|x_2|}]^\\top\\}$, $B(x)=x_2$, and $K=\\{x_2\\le 0\\}$. The boundary inequality $\\langle\\nabla B(x),F(x)\\rangle=0$ holds on $\\partial K$, yet the solution $x(t)=(t,\\frac14 t^2)$ starts in $K$ and leaves it. This example shows that a boundary-only certificate must exclude such flows, and condition (21) is precisely the exclusion; a variant satisfying (21) while still admitting a leaving solution would falsify Theorem 2.","tokens_in":35506,"feed_emoji":"🛡️","tokens_out":7497,"duration_ms":80625,"temperature":0.7,"pith_summary":"This paper establishes sufficient conditions, expressed as infinitesimal inequalities, under which a closed set is forward pre-invariant or pre-contractive for a hybrid inclusion. The set is defined as the common region where several scalar functions—the barrier function candidate—are nonpositive, so safety constraints with multiple simultaneous requirements can be certified without flattening them into one nonsmooth scalar. Pre-invariance means every maximal solution starting in the set stays in it; pre-contractivity means solutions starting on the boundary immediately move to the interior. The conditions separate into flow constraints, checked on an outer neighborhood of each constraint's zero level set using the contingent cone of admissible directions, and jump constraints ensuring jumps land back in the union of flow and jump sets. The payoff is a certificate that avoids computing solutions, even when solutions are nonunique or terminate prematurely.","feed_headline":"Barrier inequalities certify safety in hybrid systems","feed_subtitle":"Multiple scalar conditions keep solutions inside a target set through flows and jumps, no trajectories needed.","key_machinery":"The central object is a vector-valued barrier function candidate $B=(B_1,\\dots,B_m)$ defining $K=\\{x\\in C\\cup D: B(x)\\le 0\\}$. The argument runs on the active zero-level sets $M_i=\\{x\\in\\partial K: B_i(x)=0\\}$: the flow condition is checked only on an outer neighborhood $(U(M_i)\\setminus K_{e_i})\\cap C$, intersected with the contingent cone $T_C(x)$ of directions along which solutions can flow while staying in $C$. For contractivity, strict inequality together with the Dubovitsky-Miliutin cone forces flows to enter $\\operatorname{int}(K)$. The boundary-only variant in Theorem 2 replaces the neighborhood check by a condition on $\\partial K$ using a transversality assumption and inequality (21), a one-sided Lipschitz-like condition involving a uniqueness function $\\rho$.","core_discovery":"The central claim is Theorem 1: given a $C^1$ vector barrier function candidate $B$ defining $K=\\{x\\in C\\cup D: B(x)\\le 0\\}$, the set $K$ is forward pre-invariant if, for each component $i$, every flow direction $\\eta\\in F(x)\\cap T_C(x)$ satisfies $\\langle\\nabla B_i(x),\\eta\\rangle\\le 0$ on an outer neighborhood $(U(M_i)\\setminus K_{e_i})\\cap C$, and if every jump from $x\\in D\\cap K$ satisfies $B(\\eta)\\le 0$ for $\\eta\\in G(x)$ together with $G(x)\\subset C\\cup D$. The paper extends this to locally Lipschitz barrier functions using Clarke generalized gradients, relaxes the flow inequality to $\\langle\\nabla B_i(x),\\eta\\rangle\\le \\rho(B_i(x))$ with $\\rho$ a uniqueness function, and provides boundary-only sufficient conditions under a transversality assumption and a one-sided Lipschitz-like condition on the flow map. For contractivity, strict inequalities and a non-tangentiality condition force solutions from the boundary to enter the interior of $K$.","pith_inferences":["An extension the authors leave implicit is that the componentwise flow check could be combined with control synthesis, so a hybrid controller can enforce safety online by selecting flow inputs that satisfy the inequalities in (12).","A testable next step is to turn the sufficient conditions into an algorithmic search over polynomial barrier candidates using convex optimization; if a certificate is found, the theorems give a formal safety proof.","The boundary-only Theorem 2 relies on condition (21) being applied to a projection $y_1$ that is only argued to lie in either $\\partial K_e\\cap C$ or an exceptional set; a reader should check whether that projection is always admissible, since a gap there would restrict the theorem's validity to cases where the projection falls on $\\partial(K\\cap C)$.","Because the paper only proposes sufficient conditions, the examples showing failure when extra assumptions are dropped suggest that necessity would require different, likely cone-based, conditions; a systematic comparison of conservatism between Theorem 1 and Theorem 2 remains open."],"forward_implications":["If the conditions hold, a safety region for a hybrid inclusion is certified without simulating or computing solutions, even when flows are set-valued and solutions may stop after finite hybrid time.","Multiple constraints can be handled componentwise; the active zero-level sets $M_i$ are checked separately, avoiding the need for a single smooth scalarization of an intersection of constraints.","The relaxed flow condition with uniqueness functions allows non-Lipschitz flows, such as those with $\\rho(\\omega)=\\omega\\log\\omega$, to be covered by the pre-invariance certificate.","For contractive sets, the same machinery yields certificates that boundary states evolve inward, which is the ingredient behind set-induced Lyapunov functions and safety-plus-convergence designs.","The results apply directly to hybrid automata by encoding the mode as a discrete state, so mode-dependent safety sets can be certified with one barrier candidate per mode."],"supporting_citations":[{"why":"Supplies the viability-theoretic cone conditions (contingent, external, Dubovitsky-Miliutin) that the barrier conditions are compared against and used in the proofs.","marker":"[9]"},{"why":"Provides the notion of forward pre-invariance for hybrid inclusions and the cone-based invariance result that this paper extends.","marker":"[16]"},{"why":"Supplies the scalar control-barrier-function framework for continuous dynamics whose flow condition the paper generalizes to hybrid inclusions.","marker":"[17]"},{"why":"Is the source for contractivity via Minkowski functionals and set-induced Lyapunov functions, which motivates the contractivity definitions.","marker":"[8]"},{"why":"Is the source of uniqueness functions, used to relax the flow inequality and to state condition (21).","marker":"[39]"},{"why":"Nagumo's invariance theorem provides the boundary tangent condition that motivates the flow conditions on the boundary.","marker":"[13]"},{"why":"Defines hybrid inclusions, hybrid time domains, and solutions, and supplies the standing basic regularity assumptions.","marker":"[32]"},{"why":"Provides barrier-certificate safety verification for hybrid automata, which the multi-mode construction extends.","marker":"[20]"},{"why":"Supplies relaxed barrier-certificate conditions for hybrid automata that Proposition 1 extends to hybrid inclusions.","marker":"[23, 24]"}],"fun_headline_variants":["Barrier functions guarantee invariance in hybrid inclusions","Tight conditions for hybrid set invariance via barriers","Multiple barriers enforce forward invariance in hybrid systems","Barrier-based criteria for hybrid contractivity and invariance","Barrier inequalities ensure hybrid solutions stay in set"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument hinges on the assertion that infinitesimal inequalities checked just outside the set, or on its boundary under the extra regularity condition, rule out every possible way a solution could slip outside; if some direction of escape is not captured by the active barrier functions and the contingent cone, the certificate can fail.","fun_headline_variants_meta":{"raw":{"variants":["Barrier functions guarantee invariance in hybrid inclusions","Tight conditions for hybrid set invariance via barriers","Multiple barriers enforce forward invariance in hybrid systems","Barrier-based criteria for hybrid contractivity and invariance","Barrier inequalities ensure hybrid solutions stay in set"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000156,"raw_usage":{"total_tokens":1202,"prompt_tokens":914,"completion_tokens":288,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":530,"completion_tokens_details":{"reasoning_tokens":218}},"tokens_in":530,"tokens_out":288,"duration_ms":3523,"temperature":1.0,"reasoning_tokens":218,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:57:04.113153+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Consider the differential inclusion with $C=\\mathbb{R}^2$, $D=\\emptyset$, $F(x)=\\{[1,\\sqrt{|x_2|}]^\\top\\}$, $B(x)=x_2$, and $K=\\{x_2\\le 0\\}$. The boundary inequality $\\langle\\nabla B(x),F(x)\\rangle=0$ holds on $\\partial K$, yet the solution $x(t)=(t,\\frac14 t^2)$ starts in $K$ and leaves it. This example shows that a boundary-only certificate must exclude such flows, and condition (21) is precisely the exclusion; a variant satisfying (21) while still admitting a leaving solution would falsify Theorem 2.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the viability-theoretic cone conditions (contingent, external, Dubovitsky-Miliutin) that the barrier conditions are compared against and used in the proofs."},{"cited_title":"Chai and R","cited_arxiv_id":null,"evidence_quote":"Provides the notion of forward pre-invariance for hybrid inclusions and the cone-based invariance result that this paper extends."},{"cited_title":"Blanchini","cited_arxiv_id":null,"evidence_quote":"Is the source for contractivity via Minkowski functionals and set-induced Lyapunov functions, which motivates the contractivity definitions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Is the source of uniqueness functions, used to relax the flow inequality and to state condition (21)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Nagumo's invariance theorem provides the boundary tangent condition that motivates the flow conditions on the boundary."},{"cited_title":"Goebel, R","cited_arxiv_id":null,"evidence_quote":"Defines hybrid inclusions, hybrid time domains, and solutions, and supplies the standing basic regularity assumptions."},{"cited_title":"Prajna, A","cited_arxiv_id":null,"evidence_quote":"Provides barrier-certificate safety verification for hybrid automata, which the multi-mode construction extends."}],"review_version":1}