{"id":"e1aadcfb-cc35-4339-b5fa-1e90cb11aef6","arxiv_id":"1908.06633","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"A subclass with only upper-bound invariants is claimed to make parametric reachability easy and exactly synthesizable, but negative constant offsets break the proof.","lead":"The paper defines a restricted class of parametric timed automata that keep only location invariants and claims fast reachability checking with exact parameter synthesis. It also shows a nested temporal logic becomes undecidable on this class, but the reachability proof misses negative constant offsets.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Definition 5 permits negative integer offsets d, so Lemma 3's zero/nonzero equivalence fails even for valuations with positive parameters.","rationale":"The reader's REJECT verdict is well founded. The weakest assumption is exactly where the paper breaks: Lemmas 2 and 3 collapse because Definition 5 allows negative d. The counterexample is minimal and uses only the stated syntax, so this is not a disagreement with a convention but an internal inconsistency between Definition 5 and the proof of Lemma 3. The paper's own Theorem 2 proof notices only the x<0 blocking case caused by p=0 and misses cases like x<-2 caused by negative offsets. The undecidability reduction in Section III and the TCTL undecidability result in Section IV-B do not depend on this step, so those parts may survive; however, the main positive contribution, exact synthesis, is invalid for the submitted class. The intended repair—restricting offsets to N or otherwise excluding negative constants—would be a substantive change to the definition, not a cosmetic fix. I agree with the reader that the paper is not acceptable as stated; no adjustment to the reader's verdict is needed.","tokens_in":17014,"tokens_out":5278,"duration_ms":56819,"concrete_test":"Construct A = ({ℓ0, ℓf}, ..., I(ℓf): x < p - 2, edge ℓ0 → ℓf with true guard). Apply the paper's algorithm: it tests v(p)=0 and v(p)=1. For both, the invariant is x<-2 or x<-1 and is violated immediately, so the algorithm returns ∅. Directly check p=3: start at (ℓ0,0), take the unguarded edge to (ℓf,0), where 0<1 satisfies I(ℓf); hence ℓf is reachable. The correct EF-synthesis is p>2, so the algorithm's empty result is wrong. This single automaton simultaneously falsifies Lemmas 2 and 3 and Theorems 2 and 3.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition 5 defines PTA^U_I invariants as x ⊳ Σ α_i p_i + d with d ∈ Z, and parameter valuations range over Q+. Lemma 3 asserts that any two valuations with the same zero/nonzero pattern have identical reachability. This is false when d < 0. Let A have locations ℓ0, ℓf, an unguarded edge ℓ0 → ℓf, and invariant I(ℓf): x < p - 2. For v(p)=3, at clock value 0 the invariant x<1 holds, so a zero-delay run exists and ℓf is reachable. For v'(p)=1, the invariant becomes x<-1, which no clock valuation can satisfy since clocks are nonnegative, so ℓf is not reachable. Yet v(p)>0 and v'(p)>0, hence v ∼ v'. Thus Lemma 3 is false, Lemma 2's v1 test is false (v1(p)=1 vs v(p)=3), and the 2^{|P|} region enumeration in Theorem 3 does not compute EF-synthesis. The exact synthesis set for this automaton is p>2, not the union of zero-pattern regions. The root cause is the unstated restriction that offsets d be nonnegative; with d ≥ 0 the argument would go through, but that restriction is absent from the paper's syntax.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a syntactic subclass of parametric timed automata called PTA^U_I, in which transitions have no guards and location invariants are restricted to upper-bound constraints of the form x ⊳ Σ α_i p_i + d. It claims three main results: (1) arbitrary PTAs can be encoded by invariant-only automata, so EF-emptiness remains undecidable for PTAs with only invariants; (2) for PTA^U_I, EF-emptiness is decidable in NLOGSPACE and exact EF-synthesis is computable in exponential time by testing one valuation per zero/nonzero parameter pattern; and (3) TCTL-emptiness, in particular EGAF=0-emptiness, is undecidable for bounded PTA^U_I. The paper also reports a small case study of a media streaming protocol.","tokens_in":17232,"tokens_out":8015,"duration_ms":79483,"significance":"If the central results were correct, the paper would be significant: it would give the first exact EF-synthesis over unbounded rational-valued parameters for a nontrivial subclass of PTAs, at exponential cost, together with an undecidability boundary for TCTL. The guard-to-invariant translation in Section III is clean and appears correct, and the TCTL gadget construction in Section IV.B is substantial. However, the decidability and synthesis claims are false under the paper's own definitions. The root cause is that Definition 5 allows constant offsets d ∈ Z, including negative offsets, while Lemmas 2 and 3 assume only the zero/nonzero pattern of parameters matters. A one-clock, one-parameter counterexample directly contradicts both lemmas and invalidates the algorithm of Theorem 3. As stated, the paper's main positive contribution is not defensible.","major_comments":[{"comment":"Lemma 2 is false under the syntax actually defined in the paper. Definition 5 allows invariants of the form x ⊳ Σ α_i p_i + d with d ∈ Z, and Section II.A defines d ∈ Z with no nonnegativity restriction. The proof of Lemma 2 only discusses blockers of the form x < p with v(p) = 0 and then concludes that v1(A) has no blocking invariant because all parameters evaluate to 1; this ignores negative constant offsets. Concretely, let A have locations ℓ0 and ℓf, an unguarded transition ℓ0 → ℓf, and invariant I(ℓf) : x < p − 2. For v(p) = 3, the transition can be taken at clock value 0 because x < 1 holds, so ℓf is reachable. For v1(p) = 1, the invariant becomes x < −1, which no nonnegative clock valuation satisfies, so ℓf is unreachable. Thus the equivalence in Lemma 2 fails, and the NLOGSPACE decision procedure of Theorem 2, which tests only v1(A) using a syntactic check for invariants of the form x < 0, is not a correct decision procedure for EF-emptiness of PTA^U_I as defined.","section":"§IV.A, Definition 5 and Lemma 2"},{"comment":"Lemma 3 is also false, and this invalidates the EF-synthesis claim of Theorem 3. Using the same automaton as in the previous comment, take v(p) = 3 and v'(p) = 1. The two valuations are equivalent under Definition 6 because both parameters are positive. There is a zero-delay run reaching ℓf in v(A), since x = 0 satisfies x < 1, but there is no run in v'(A) reaching ℓf, since the invariant x < −1 is unsatifiable for all nonnegative clock values. Therefore the zero/nonzero pattern of parameter values does not determine reachability, and the 2^{|P|} regions of Definition 6 do not refine the exact synthesis set. For this automaton the exact EF-synthesis set is {v ∈ Q+ | v(p) > 2}, which is neither of the regions p = 0 or p > 0. The argument would go through under an additional restriction d ≥ 0, but no such restriction appears in Definition 5 or anywhere else in Section II.","section":"§IV.A, Lemma 3 and Theorem 3"}],"minor_comments":[{"comment":"The text says 'we focus on EF(askMore, notSending)-synthesis' and then states that the result is 'the set of valuations for which all runs eventually reach' the location; that property is AF, not EF, so the modal terminology should be corrected.","section":"§V, final paragraph"},{"comment":"The definition lists S = {(ℓ,w) ∈ L × R_+^H | w |= v(I(ℓ))} and then separately lists s0 = (ℓ0, ⃗0); it should state explicitly that the initial state is required to belong to S, or that the initial invariant is assumed satisfiable.","section":"Definition 2"},{"comment":"The sentence 'Once in ℓ1′, we cannot stay forever because of I(ℓ1′)' is not literally true for tautological guards such as x ≥ 0; the induction only needs the run to take the second transition immediately, so the sentence should be reworded to avoid claiming that the invariant forces progress.","section":"Lemma 1 proof"}],"recommendation":"reject","confidential_remarks":"The central decidability and synthesis results are false under the paper's own Definition 5. The flaw is local — a restriction to nonnegative constant offsets would likely restore Lemmas 2 and 3 — but that restriction is a substantive change to the model and would narrow the claimed scope. I recommend rejection; a resubmission with a corrected definition and correspondingly re-derived claims could be considered."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, the central decidability and synthesis theorems for PTA^U_I are false as stated. Second, the mistake is localized and the paper is probably repairable.\n\nThe genuinely new idea is the guard-to-invariant encoding: a PTA without invariants can be turned into a PTA with only invariants, preserving reachability, so the invariant-only class inherits undecidability. I checked Lemma 1; it works. The paper then defines PTA^U_I, invariants of the form x ⊳ Σ α_i p_i + d, and claims EF-emptiness is NLOGSPACE and EF-synthesis can be computed exactly in exponential time by enumerating zero/nonzero patterns of valuations. That would be a real improvement over L/U-PTAs, which lack exact synthesis.\n\nThe problem is Definition 5. It allows d ∈ Z. The lemmas only hold if d ≥ 0. Here is a concrete failure: one clock x, one parameter p, initial location with no invariant, a single transition to goal with invariant x < p - 2. For v(p)=3, at clock value 0 the invariant x<1 holds, so the goal is reachable by a zero-delay run. For v'(p)=1, the invariant is x<-1, unsatisfiable for any nonnegative clock. Both valuations have the same zero/nonzero pattern, so Lemma 3's equivalence fails, and Lemma 2 fails too because v1(p)=1 gives the unsatisfiable invariant while v(p)=3 gives a satisfiable one. Hence Theorems 2 and 3 collapse. The exact synthesis set for this tiny automaton is p>2, not a union of zero-pattern regions.\n\nIf the authors restrict d to N, the monotonicity argument goes through: with d≥0, satisfiability of an upper-bound invariant at clock value 0 is determined exactly by whether the expression is zero or positive, which is the zero-pattern information. So the claimed results are likely recoverable by a small syntactic repair. That does not rescue the paper as written; the counterexample is directly under the stated definition, and the proofs of Lemmas 2 and 3 explicitly rely on the false claim that nothing can block a zero-delay run. The TCTL undecidability reduction uses only nonnegative offsets, so it is not affected.\n\nWho is this for? People working on parametric timed automata who care about subclass taxonomy and exact synthesis. The paper is clearly written and the failure mode is instructive. It deserves peer review because the idea is valuable and the fix is identifiable, but the current version should be rejected or returned for revision.","headline":"The paper's core reachability and synthesis theorems are false under its own syntax—negative offset constants break the zero-pattern lemmas—but the guard-to-invariant encoding is sound and the main results are likely repairable by restricting constants to nonnegative integers.","tokens_in":17798,"tokens_out":3883,"would_cite":false,"duration_ms":39779,"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":"Removing guards from parametric timed automata leaves reachability decidable and yields exact parameter synthesis in exponential time.","keywords":["parametric timed automata","invariants","reachability synthesis","decidability","TCTL","upper-bound constraints","exact parameter synthesis","timed automata"],"falsifier":"Under the paper's own definition $d \\in \\mathbb{Z}$, let the target location have invariant $x < p - 2$ and no resets, with an unguarded edge from the initial location to it. For $p=3$ the location is immediately reachable because $x=0<1$; for $p=1$ the same sign pattern ($p>0$) gives the invariant $x < -1$, which no clock value can satisfy, so no run exists. This contradicts the paper's lemma that equal zero/nonzero patterns give equal reachability.","tokens_in":16754,"feed_emoji":"⏱️","tokens_out":11167,"duration_ms":105498,"temperature":0.7,"pith_summary":"This paper proposes a syntactic restriction of parametric timed automata in which transitions carry no guards, so timing constraints live only in location invariants. It shows that the unrestricted invariant-only version is still as expressive as full parametric timed automata and inherits their undecidability, but that a further restriction to upper-bound constraints makes the reachability (EF) emptiness problem decidable in NLOGSPACE and, more strongly, makes exact synthesis of all rational parameter valuations that reach a target location computable in exponential time. The paper also proves that full TCTL emptiness is undecidable for this same subclass, placing it at a boundary between decidability and undecidability. A small media-streaming case study illustrates the synthesis result.","feed_headline":"Removing guards from parametric timed automata yields exact synthesis","feed_subtitle":"For reachability, a guard-free subclass computes every rational parameter valuation that reaches a target state.","key_machinery":"The central object is the class $\\mathrm{PTA}^U_I$: parametric timed automata with no guards and with only upper-bound invariants, meaning every location constraint is of the form $x \\lhd \\sum_i \\alpha_i p_i + d$ with $\\lhd \\in \\{<,\\leq\\}$, $\\alpha_i \\in \\{0,1\\}$, and $d \\in \\mathbb{Z}$. The argument is carried by two lemmas showing that any successful run can be compressed to a zero-delay run, and that the existence of a zero-delay run is unchanged when each parameter is replaced while preserving whether it is zero or positive. This reduces EF-emptiness to NLOGSPACE reachability in a directed graph and EF-synthesis to enumerating $2^{|P|}$ representative parameter valuations.","core_discovery":"The central discovery is a collapse in behavior: for a parametric timed automaton whose only constraints are upper-bound location invariants (each inequality of the form $x \\lhd \\sum_i \\alpha_i p_i + d$ with $\\lhd \\in \\{<,\\leq\\}$), the existence of some parameter valuation that reaches a given location is decided by zero-delay reachability in the non-parametric automaton where every parameter equals 1. More generally, whether a zero-delay path exists depends only on the zero/nonzero pattern of the parameter values, so the parameter space splits into at most $2^{|P|}$ regions. Testing one representative valuation per region yields an exact description of the EF-synthesis set, in exponential time and over unbounded rational parameters; the paper presents this as the first such exact synthesis result in this line of work without restrictions on clock count, parameter count, or resets.","pith_inferences":["The $2^{|P|}$-region classification works only if the integer offsets $d$ in upper-bound invariants are nonnegative; the paper never states this, and with a negative offset the equivalence fails: an invariant $x < p - 2$ admits a zero-delay run for $p=3$ but not for $p=1$, although both have $p>0$.","If the classification holds, every EF-synthesis set for $\\mathrm{PTA}^U_I$ is a finite union of orthants defined by $p=0$ versus $p>0$, so the exact synthesis result has very simple geometry and could be checked by sign tests alone.","The guard-to-invariant compilation suggests a general recipe: for reachability questions, any PTA can be rewritten as an invariant-only automaton with twice as many edges, though undecidability of the target class means this translation cannot produce a decision procedure by itself.","A testable extension is whether AF-emptiness also respects the same zero/nonzero regions; the paper leaves flat TCTL formulas such as AF, EG, and AG open, and universal quantification over runs may break the collapse."],"forward_implications":["EF-emptiness for $\\mathrm{PTA}^U_I$ is decidable in NLOGSPACE: it suffices to check zero-delay reachability in the automaton with all parameters set to 1.","EF-synthesis is exactly computable in exponential time, producing a finite union of regions of the form $p=0$ or $p>0$ for each parameter; this covers unbounded rational parameters.","Every guard can be compiled into an invariant by splitting the guarded edge into two unguarded edges through a fresh location, so invariant-only automata are as expressive as full PTAs and EF-emptiness for them is undecidable.","For bounded $\\mathrm{PTA}^U_I$, the nested TCTL formula $\\mathrm{EGAF}_{=0}$ can simulate a two-counter machine, making TCTL-emptiness undecidable in the class.","In the case study, the protocol's bad state is reachable under every valuation with $p_{\\mathrm{send}}>0$ and $p_{\\mathrm{rced}}>0$, while no valuation makes the bad state unavoidable on all runs."],"supporting_citations":[{"why":"Introduces parametric timed automata and supplies the undecidability of EF-emptiness that the guard-removal result inherits.","marker":"[AHV93]"},{"why":"Provides the timed automaton semantics of clocks, delays, and resets that the zero-delay compression argument operates on.","marker":"[AD94]"},{"why":"Defines U-PTAs and gives the decidable EF-emptiness and integer-synthesis baseline that the new rational synthesis result extends.","marker":"[BL09]"},{"why":"Proves EF-synthesis intractable for L/U-PTAs, motivating the exact-synthesis contribution.","marker":"[JLR15]"},{"why":"Provides the two-counter machine encoding that the TCTL undecidability proof adapts into $\\mathrm{PTA}^U_I$ gadgets.","marker":"[ALR16]"},{"why":"Shows EGAF=0-emptiness undecidable for U-PTAs, the technique reused here for TCTL-emptiness.","marker":"[ALR18]"},{"why":"Establishes undecidability of boundedness for two-counter machines, the source of the reduction in Theorem 4.","marker":"[KC10]"},{"why":"Gives the reset-PTA class with exact synthesis only for bounded parameters, the comparison point for unbounded synthesis.","marker":"[ALR19]"},{"why":"Supplies the NLOGSPACE graph-reachability result that Theorem 2 reduces EF-emptiness to.","marker":"[Pap94]"}],"fun_headline_variants":["Guard-free PTAs: exact reachability synthesis in exponential time","Removing guards yields exact synthesis for reachability","Zero-delay tests decide reachability for invariant-only PTAs","Exact EF-synthesis: invariant-only PTAs in exponential time"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole construction depends on the assumption that two parameter choices with the same zero-versus-positive pattern always allow the same no-time-elapse paths; this requires the fixed integer offsets in upper-bound invariants never to make one such choice block a path that another choice in the same pattern admits.","fun_headline_variants_meta":{"raw":{"variants":["Guard-free PTAs: exact reachability synthesis in exponential time","Removing guards yields exact synthesis for reachability","Zero-delay tests decide reachability for invariant-only PTAs","Exact EF-synthesis: invariant-only PTAs in exponential time"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000497,"raw_usage":{"total_tokens":2436,"prompt_tokens":947,"completion_tokens":1489,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":563,"completion_tokens_details":{"reasoning_tokens":1432}},"tokens_in":563,"tokens_out":1489,"duration_ms":10040,"temperature":1.0,"reasoning_tokens":1432,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T12:40:13.243263+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Under the paper's own definition $d \\in \\mathbb{Z}$, let the target location have invariant $x < p - 2$ and no resets, with an unguarded edge from the initial location to it. For $p=3$ the location is immediately reachable because $x=0<1$; for $p=1$ the same sign pattern ($p>0$) gives the invariant $x < -1$, which no clock value can satisfy, so no run exists. This contradicts the paper's lemma that equal zero/nonzero patterns give equal reachability.","supporting_citations":[],"review_version":1}