{"id":"69e18c03-ceae-432d-b6fe-b8a730359208","arxiv_id":"1908.04750","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":4,"one_line_summary":"A self-triggered controller for reachability and safety specifications is synthesized via symbolic abstractions and a reachability game, with validity guaranteed when an abstract winning set covers the initial states.","lead":"The authors propose a method to automatically design self-triggered controllers for nonlinear systems that must reach a target region while avoiding obstacles. The approach uses symbolic models and reachability games, and works without stability assumptions or convex safety sets.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's proof has an unproven induction step: the nearest abstract state used by controller (8) may not continue the abstract winning trajectory, so rank decrease is not guaranteed.","rationale":"The paper's central contribution is Theorem 1, claiming that the memoryless refined controller (8) is valid whenever X0⊆PS. The reader's conditional verdict focuses on the practical difficulty of achieving X0⊆PS. My stress test identifies a more fundamental issue: the proof of Theorem 1 does not show that the controller's own choice of abstract state (the nearest point in ~P_S) follows the abstract winning strategy. The proof uses an existential successor from the alternating simulation relation to maintain the rank decrease, but the actual controller at the next step is defined via a different abstract state. Since the rank L is an arbitrary ranking on a finite set, nothing prevents the nearest abstract state from having a larger rank, and the sequence of nearest abstract states need not be an abstract trajectory. Thus Lemma 3 cannot be applied inductively. This is not a disagreement with the consensus on abstraction-based control; it is an internal gap in the argument. The concern is testable: if one re-derives the induction step with the nearest-point selection, the required inequality is not a consequence of (7) and (8). The proposed concrete test would settle it analytically or by a small counterexample. If the gap is confirmed, the paper's main theorem is unproven; a corrected controller (e.g., choosing the related abstract state with minimal L, or equipping the controller with memory of the abstract witness) would likely restore the result. I therefore recommend UNVERDICTED rather than CONDITIONAL, since the correctness of the central claim is not established as written.","tokens_in":12182,"tokens_out":20995,"duration_ms":229147,"concrete_test":"Independently prove the induction step of Theorem 1 with Nearest_{~P_S}(x_{k+1}) replacing the existential D3 witness; show L(Nearest_{~P_S}(x_{k+1})) < L(Nearest_{~P_S}(x_k)) follows from (7) and (8). If the step fails, construct a one-dimensional lattice with η_x=1, ε=1 and a reachability game whose rank function has adjacent values 1 and 5, simulate controller (8) from a concrete state closer to the rank-1 node, and check whether the rank of the nearest abstract state increases along the closed loop. One increase invalidates the proof's monotone-rank argument.","verdict_should_be":"UNVERDICTED","load_bearing_attack":"Theorem 1 (Section IV) is not established by its proof. The proof chooses the abstract state ~x_{k0}=Nearest_{~P_S}(x_{k0}) with rank L(~x_{k0})=N, applies an action from ~C(~x_{k0}), and via the strong ε-ASR (D3) obtains an existential abstract successor ~z_{k1}∈P(N−1) related to the concrete successor x_{k1}. The proof then says 'by recursively applying the above procedure.' But the recursive step must pick Nearest_{~P_S}(x_{k1}), which need not equal ~z_{k1}. Nothing in (7), (8), or Definition 5 implies L(Nearest_{~P_S}(x_{k1})) < L(~x_{k0}): the rank function L on the finite lattice can vary arbitrarily between adjacent abstract states, and the closest state to x_{k1} may have a larger rank than the existential witness. Consequently, the sequence of abstract states actually used by the memoryless controller (8) need not be a trajectory of ~Σ_A, and Lemma 3's rank-decrease argument does not transfer. A modified controller that selects the related abstract state with minimal L, or one with memory of the previous abstract state, would fix the argument, but as written the condition X0⊆PS does not guarantee validity of (8).","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a symbolic-model method for synthesizing self-triggered controllers for nonlinear discrete-time systems subject to reachability and safety specifications. It constructs an augmented transition system for the plant, quantizes it to a finite symbolic model, establishes a strong approximate alternating simulation relation (Lemma 2), solves a reachability game on the abstraction (Algorithm 1) to obtain an abstract winning set and a rank function, and then refines the abstract controller to a memoryless self-triggered controller via Eq. (8). Theorem 1 claims that if all concrete initial states lie within precision ε of the abstract winning set, the refined controller guarantees finite-time reachability of the target set and invariance of the safety set. A numerical vehicle example illustrates the approach and reports aperiodic communication.","tokens_in":12463,"tokens_out":10302,"duration_ms":116173,"significance":"If the central theorem were correct, the paper would contribute a useful abstraction-based synthesis method for self-triggered control with non-convex safety sets, requiring only Lipschitz continuity rather than stability or contractivity assumptions. The construction of the symbolic model and the proof of Lemma 2 are technically sound, and Algorithm 1 is a standard and appropriate fixpoint scheme for the abstract reachability-safety game. The numerical example demonstrates the intended behavior. However, the refinement step in Theorem 1 is not established as written: the memoryless nearest-state selection can break the rank-decrease argument on which the finite-time guarantee rests. The flaw is repairable, but the paper's main guarantee currently lacks a valid proof.","major_comments":[{"comment":"The proof of Theorem 1 has an invalid induction step. In the first step the proof picks ~x_k0 ∈ Nearest_{~P_S}(x_k0) with rank N and uses the strong ε-ASR to obtain an existential abstract successor ~x_k1 ∈ P(N−1) that is related to the concrete successor x_k1. It then says to repeat the procedure from k1. The repeat step, however, must choose Nearest_{~P_S}(x_k1), and nothing in Definition 5, Eq. (7), or Eq. (8) guarantees that this nearest point has rank at most N−1; the rank function L on the finite lattice can vary arbitrarily between nearby abstract states, so the selected point may have rank N or larger. Consequently the sequence of abstract states actually used by the memoryless controller (8) need not be a trajectory of ~ΣA with decreasing L, and Lemma 3 does not apply recursively. A correct refinement would need to choose, for example, an abstract state of minimal rank among those within ε of the concrete state, or to carry the previous abstract state as memory.","section":"Section IV, Theorem 1 (Eq. (8))"},{"comment":"Even if the rank of the nearest abstract state were controlled at the first step, the controller C(x) in Eq. (8) is the union of ~C(~x) over all ~x ∈ Nearest_{~P_S}(x). Since different nearest points can have different ranks, a controlled trajectory in the sense of Definition 1, which quantifies over all possible induced trajectories, could at every communication instant select an action coming from a high-rank nearest point. The proof of Theorem 1 silently fixes one abstract state, but the nondeterminism in (8) is not resolved by the controller definition.","section":"Section IV, Definition 1 and Eq. (8)"}],"minor_comments":[{"comment":"The sentence 'Even though X0 ⊈PS does not hold' is confusing and should presumably read 'Even if X0⊆PS does not hold, one might still be interested...'.","section":"Remark 2"},{"comment":"The input pair (u′, m′) is introduced in the proof, but the safety condition is later written with (u, m) without primes; this notational slip should be corrected.","section":"Proof of Lemma 3"},{"comment":"The phrase 'with 6 number of communication times' should be reworded, for example as 'with 6 communication events'.","section":"Section V"}],"recommendation":"major_revision","confidential_remarks":"The stress-test concern is confirmed by the manuscript text: Theorem 1's proof does not control the rank of Nearest_{~P_S} at successive communication instants, so the central refinement guarantee is not proven as written. The gap is fixable by changing the refinement map to select a minimal-rank eligible abstract state or by adding memory of the abstract state, and the rest of the abstraction machinery appears sound. Therefore I recommend major revision rather than rejection. The authors should also be asked to clarify the non-constructive nature of the condition X0⊆PS and the parameter-selection limitations acknowledged in Remarks 1 and 2."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read this one if you care about symbolic-model synthesis for networked control. The genuinely new piece is the augmented transition system: the controller chooses the inter-communication interval m together with u, and the symbolic model is built over the joint (u,m) decisions with precision ε_m = L_x^m ε + η_x. That is a natural but non-obvious move, and it is what lets them treat non-convex safety sets without stability assumptions. I agree with the reader that Lemma 2 and the engineering of the abstraction are sound; the quantization error propagation through the Lipschitz bound is clean.\n\nThe soft spots are two. First, the main theorem's proof has a gap, and the stress-test note is right. At each round the concrete controller (8) looks at Nearest_{~P_S}(x_k), but the induction in Theorem 1 uses the abstract successor produced by the simulation relation. These need not be the same abstract state, and nothing forces the rank to decrease when you switch to the nearest one. The rank function can jump upward between neighboring lattice states, so the memoryless controller may not follow a winning abstract trajectory. This is a load-bearing gap: X_0 ⊆ P_S plus a valid abstract controller is not enough, as written, to guarantee finite-time reachability. It is fixable — use memory, or select the successor as part of the control decision — but the authors need to say which.\n\nSecond, the design relies on the condition X_0 ⊆ P_S, and there is no constructive way to choose η_x, η_u, ε, M_max to make it hold. The paper admits this in Remarks 1-2 and lists the parameter search as future work. That is a practical rather than logical weakness, but it matters because the only numerical example took 20,760 seconds for a two-dimensional system and no code or data is included to reproduce it.\n\nCitation pattern is fine; the self-citations are on point. I would not desk-reject this. The construction is novel and the reachability-game formulation is competent. But the proof gap in Theorem 1 must be fixed before the result can be accepted, and the parameter-selection issue should at least get a systematic discussion. A serious referee would be doing useful work.","headline":"A genuinely new abstraction for self-triggered control, but the proof of the main theorem has a real gap; worth refereeing, not ready as is.","tokens_in":699,"tokens_out":1036,"would_cite":true,"duration_ms":45976,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C55","93B03","93C65","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Self-triggered control proven via symbolic reachability games","keywords":["self-triggered control","symbolic models","reachability and safety","networked control systems","approximate alternating simulation","reachability game","nonlinear control","non-convex safety sets"],"falsifier":"Simulate the refined controller for any Lipschitz system with verified X0 ⊆ PS; a single trajectory that exits XS before reaching XF would refute Theorem 1.","tokens_in":11989,"feed_emoji":"🎮","tokens_out":4846,"duration_ms":48056,"temperature":0.7,"pith_summary":"This paper proposes a way to synthesize self-triggered controllers for nonlinear discrete-time control systems that must reach a target while never leaving a safety set, even when the safety set is non-convex. The approach builds a finite symbolic model of the system by quantizing states and inputs and bounding how far trajectories can drift over a fixed horizon, then solves a reachability game on that model. Winning abstract states are refined back to the original system: a concrete state quantizes to a winning abstract state, and the controller applies the abstract input and waits the abstract time. The paper proves that if every initial state lies in the winning region PS, the refined controller guarantees finite-time reachability and safety. The only assumption on the plant is Lipschitz continuity, so no stability or contraction condition is needed.","feed_headline":"Self-triggered control proven via symbolic reachability games","feed_subtitle":"A finite oracle built from a Lipschitz plant picks when to communicate and what to send, guaranteeing reach-and-stay.","key_machinery":"The load-bearing object is the symbolic model of Definition 5, parameterized by quantization parameters ηx, ηu, a maximum inter-communication step Mmax, and precision ε≥ηx. Its transitions are defined by over-approximating the reachable tube: an abstract successor x~+ is allowed if it lies in the ball of radius L_x^m ε + ηx around φ(x~, u~, m), the true state reached from the abstract state under constant input. This makes R(ε) = {(x~,x): ‖x~ - x‖ ≤ ε} a strong ε-ASR without requiring stability. On top of the symbolic model, Algorithm 1 iteratively computes the set ~PS of abstract states from which the target is reachable within the safety set; the controller (7) chooses inputs that strictly decrease the layer L(x~), and (8) refines this to concrete states. The mechanism that carries the argument is the combination of the simulation relation, which transfers winning abstract trajectories to concrete ones, and the ε-shrinking of XS and XF, which converts abstract safety into concrete safety.","core_discovery":"The central claim is Theorem 1: given the augmented transition system of a Lipschitz nonlinear plant, its quantized symbolic model, and a strong ε-approximate alternating simulation relation between them, the reachability-game winning set ~PS can be transferred to the plant. Define PS as all concrete states x such that some nearest abstract state is in ~PS. If the initial set X0 lies inside PS, then the controller that picks a winning abstract state nearest to the current concrete state, applies the corresponding constant input for the corresponding waiting time, is valid: every induced trajectory enters the target set in finite time and never leaves the safety set. The proof works by inductively matching each concrete transition to an abstract transition in the winning set, with the simulation relation ensuring the abstract state stays in the shrunk safety set ~XS while the concrete state stays in XS.","pith_inferences":["The condition X0 ⊆ PS is not only a proof artifact; it suggests a practical design loop where one coarsens ηx, ηu until PS covers X0, at the cost of exponential growth of the abstract state space. A dual strategy—fixing the controller and learning the coarsest admissible quantization—might be derived from the same simulation bounds.","The layer function L(x~) computed by Algorithm 1 could be reused as a runtime Lyapunov-like certificate for the closed loop, giving a data structure that monitors the remaining time-to-target without additional computation.","The over-approximation radius ε_m = L_x^m ε + ηx grows exponentially with the waiting time m, so long inter-communication steps are penalized by conservatism. This suggests an inherent trade-off between communication reduction and achievable precision that could be formalized as an optimization over Mmax.","For systems with large Lipschitz constants, the method may produce an empty ~PS even when a valid controller exists, so a natural testable extension is a parameter-adaptive scheme that locally refines the lattice only near the winning frontier."],"forward_implications":["The synthesis works for non-convex safety sets, so obstacle-filled environments in robot motion planning are directly admissible.","No Lyapunov or incremental stability assumption is needed; Lipschitz continuity suffices, expanding the class of plants beyond earlier self-triggered designs.","Communication is aperiodic: the controller outputs both the input and the waiting time, reducing the number of transmissions compared to periodic control (109 to 6 in the example).","The guarantee is conditional on X0 ⊆ PS; when the condition fails, one can still restrict to X0 ∩ PS and obtain a valid controller for that subset.","Because the symbolic model is finite, the synthesis terminates, so the same algorithm can be implemented for any discrete-time Lipschitz plant once the parameters are fixed."],"supporting_citations":[{"why":"Provides the reachability-game and symbolic-model framework that Algorithm 1 builds on.","marker":"[10]"},{"why":"Shows symbolic models can be constructed without stability assumptions, the property the paper exploits.","marker":"[15]"},{"why":"Introduces the strong approximate alternating simulation relation and symbolic design for networked control systems, the abstraction concept used here.","marker":"[16]"},{"why":"The earlier self-triggered reachability-safety design requiring a δ-ISS Lyapunov function; the comparison that motivates the new approach.","marker":"[9]"},{"why":"Defines event- and self-triggered control and the communication paradigm the controller fits.","marker":"[1]"}],"fun_headline_variants":["Self-triggered control via symbolic reachability games","Symbolic reachability games guarantee safe self-triggered control","Reach-and-stay control with self-triggering from symbolic games","Symbolic abstraction yields self-triggered safe controllers","Symbolic games pick when and what to send for safety"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The guarantee collapses if X0 ⊈ PS: the paper gives no constructive procedure for choosing the quantization and precision parameters to ensure this inclusion, and for a given plant the winning set can be empty.","fun_headline_variants_meta":{"raw":{"variants":["Self-triggered control via symbolic reachability games","Symbolic reachability games guarantee safe self-triggered control","Reach-and-stay control with self-triggering from symbolic games","Symbolic abstraction yields self-triggered safe controllers","Symbolic games pick when and what to send for safety"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000779,"raw_usage":{"total_tokens":3368,"prompt_tokens":795,"completion_tokens":2573,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":411,"completion_tokens_details":{"reasoning_tokens":2486}},"tokens_in":411,"tokens_out":2573,"duration_ms":19151,"temperature":1.0,"reasoning_tokens":2486,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:02:54.273906+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Simulate the refined controller for any Lipschitz system with verified X0 ⊆ PS; a single trajectory that exits XS before reaching XF would refute Theorem 1.","supporting_citations":[{"cited_title":"Tabuada, Verification and Control of Hybrid Systems – A Symbolic Approach, Springer, 2009","cited_arxiv_id":null,"evidence_quote":"Provides the reachability-game and symbolic-model framework that Algorithm 1 builds on."},{"cited_title":"Symbolic models for nonlinear control systems without stability assumptions,","cited_arxiv_id":null,"evidence_quote":"Shows symbolic models can be constructed without stability assumptions, the property the paper exploits."},{"cited_title":"Design of symbolic con- trollers for networked control systems,","cited_arxiv_id":null,"evidence_quote":"Introduces the strong approximate alternating simulation relation and symbolic design for networked control systems, the abstraction concept used here."},{"cited_title":"Synthesizing communication plans for reachability and safety specifications,","cited_arxiv_id":null,"evidence_quote":"The earlier self-triggered reachability-safety design requiring a δ-ISS Lyapunov function; the comparison that motivates the new approach."}],"review_version":1}