{"id":"22a786a5-5103-4915-affd-eba685e73d4e","arxiv_id":"2506.07802","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new on-the-fly symbolic algorithm with vertex merging and an expansion abstraction verifies TATL on timed multiplayer games, outperforming Uppaal Tiga by almost an order of magnitude.","lead":"This paper presents an on-the-fly algorithm that checks timed alternating-time temporal logic (TATL) properties of real-time multiplayer games, using a lazy dependency-graph framework that only explores the states needed. It introduces a way to merge equivalent graph nodes and a new abstraction that speeds up verification by roughly two orders of magnitude over the naive method in benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Equation (4)'s Forceable set puts Wϕ1 into Predλ's avoid set, so the symbolic encoding under-approximates until properties; a one-clock, no-action delay-only model would make Theorem 10 false as written.","rationale":"The reader's weakest assumption concerned the practical performance premise of the expansion abstraction. I find a more fundamental issue: the central formal claim, Theorem 10, appears to be false as written because the symbolic definitions of Forceable and Unavoidable in Equations (4) and (6) are inconsistent with their own prose definitions. The prose requires staying inside Wϕ1 (or Wϕ2) during the delay; the equation puts Wϕ1 into the set that Predλ must avoid, which makes the operator return only states that are already in the target or can jump to it without passing through Wϕ1. The one-clock no-action counterexample shows the encoding would reject a trivially true until property. This threatens both the theoretical contribution and the experimental interpretation: if the implementation uses the printed equations, its answers are unsound; if it uses the prose semantics, the paper does not describe the algorithm it evaluates. The reproducibility package is a positive signal, but it does not settle which version is implemented. Because the load-bearing correctness theorem fails as stated, I recommend rejection, or at minimum a major correction of the symbolic operator definitions and a re-verification of the experiments.","tokens_in":22556,"tokens_out":19517,"duration_ms":235459,"concrete_test":"Using the reproducibility package (Zenodo 15195408), build a TMG with one location ℓ, one clock x, invariant x≤10, no actions, and check the root state x=0 against ⟨⟨S⟩⟩(true U x≥5) with S=∅. The correct answer is true (delay to x=5). If the tool returns false, Equation (4) is what is implemented and Theorem 10 is refuted. If it returns true, inspect the implementation of ForceableS: it must be computing Predλ(Wϕ2∪PredS(W)∪H, Q\\(Wϕ2∪(Wϕ1∩safe))) or equivalent; then the printed Equation (4) is a typo and needs correction, and the proof of Theorem 10 must be reconciled.","verdict_should_be":"REJECT","load_bearing_attack":"Section 3 defines ForceableS in prose as: there exists a delay δ such that every intermediate state is in Wϕ2 or in Wϕ1 with all S-actions leading into W, and the end state is in Wϕ2 or has an S-action into W. The symbolic equation (4) instead computes Predλ(Wϕ2 ∪ PredS(W) ∪ H, [Wϕ1 ∪ PredS(W)] \\ Wϕ2). Since Predλ(Q',Q'') avoids Q'' throughout the delay (definition in §2.1), the second argument forbids every state in Wϕ1\\Wϕ2. This is the opposite of the prose: during the delay the system is required to stay in Wϕ1 until Wϕ2. Concretely, take a single location with invariant x≤10, no actions, R=[0,10], ϕ=⟨⟨S⟩⟩(true U x≥5). Prose accepts x=0 with δ=5. Equation (4) gives Predλ([5,10],[0,5)) = [5,10], so x=0 is rejected. The same inversion appears in Equation (6) for Unavoidable via the Wϕ1 term. If the implementation follows these equations, Theorem 10 is false and the abstraction theorem 18 inherits the failure; if the implementation follows the prose, the paper's central formal statement does not match the algorithm.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an on-the-fly symbolic algorithm for verifying timed alternating-time temporal logic (TATL) on timed multiplayer games, based on an encoding into extended abstract dependency graphs (EADGs). It introduces a general vertex-merging operation (derivations) that subsumes conventional inclusion checking, and proposes an \"expansion abstraction\" that replaces each zone by the full invariant zone of the location, eliminating the need for inclusion checks. The algorithm is implemented in Uppaal and evaluated on 236 queries from three benchmark families, showing substantial speedups over Uppaal Tiga on the TATL subset for which Tiga is applicable. The paper also provides a reproducibility package.","tokens_in":22803,"tokens_out":19174,"duration_ms":220754,"significance":"If the technical results are correct, the paper makes a valuable contribution: it provides the first on-the-fly EADG-based algorithm for TATL, generalizes inclusion checking to the EADG framework, and introduces an abstraction with strong experimental performance (nearly an order of magnitude faster than Uppaal Tiga in the reported configurations). The orthogonality of EADG encodings for timed games and ATL is a useful conceptual point, and the reproducibility package is a concrete strength. However, the central correctness theorem is currently undermined by an inconsistency in the symbolic characterization of the Forceable/Unavoidable operators; the value of the paper depends on repairing this defect.","major_comments":[{"comment":"The symbolic definition of ForceableS is inconsistent with the prose definition and with the semantics of Predλ given in Section 2.1. Predλ(Q',Q'') is defined as the set of states that can delay to Q' while avoiding Q''; in Eq. (4), the second argument is [Wϕ1 ∪ PredS(W)] \\ Wϕ2, which includes Wϕ1. Thus the formula forbids every state in Wϕ1 during the delay, which is the opposite of the prose requirement that the delay stay in Wϕ1 until Wϕ2. Concretely, take a one-location timed automaton with invariant x≤10, no actions, R=[0,10], and ϕ=⟨⟨S⟩⟩(true U x≥5). The prose accepts x=0 with δ=5, while Eq. (4) gives Predλ([5,10],[0,5)) = [5,10], rejecting x=0. The same inversion appears in Eq. (6) for UnavoidableS, and it propagates to the unsat encoding in Section 3.1. Consequently, Theorem 10 is false as stated, and Theorems 17 and 18 inherit the flaw.","section":"Section 3, Eq. (4) and Eq. (6)"},{"comment":"The monotonicity proof for the uses of Predλ is incorrect. The second argument of Predλ in Eq. (4) is (Wϕ1 ∪ PredS(W)) \\ Wϕ2; as a function of Wϕ1, this set is monotone increasing (a set difference with a constant subtracted set), not monotone decreasing as the proof claims. The proof's statement that \"due to the complements, this expression decreases monotonically\" is therefore unsupported. Consequently, the claim that this use of Predλ is monotonically increasing is not established, and the component decomposition on which the fixed-point computation relies is not justified.","section":"Section 3, Lemma 9"},{"comment":"The proof of Theorem 18 is only a two-line sketch. The assertion that \"effectively E(v)◦i fR = E(v) for all v\" needs a rigorous formal statement: one must prove that expanding every zone R to the full invariant JI(ℓ)K does not change the value of any value function on states in the original region R. The informal \"we assess\" remark about useless edges being rare is a performance heuristic, not a correctness argument. Since the expansion abstraction is a central contribution and is used in all experimental comparisons, a complete proof is necessary.","section":"Section 4.3, Theorem 18"},{"comment":"The proof for the ⟨⟨S⟩⟩(ϕ1Uϕ2) and JSK(ϕ1Uϕ2) cases is too terse: it says \"we get (by construction)\" without demonstrating that the symbolic value function ForceableS(Wϕ1,Wϕ2,⋃Wai) (resp. UnavoidableS) actually characterizes the semantic condition for the respective operators. Given that the error in Eq. (4) occurs precisely in that symbolic characterization, the proof must spell out the equivalence between the fixed-point computation and the semantics, rather than appealing to Lemma 11 alone.","section":"Section 3, Theorem 10 proof (Until/Unavoidable cases)"}],"minor_comments":[{"comment":"The definition of time-locked states contains a typographical artifact: \"∃ ''x≤k''∈I(ℓ)\" should be written as \"∃ (x≤k)∈I(ℓ)\". In addition, the discrete transition rule uses \"v\" instead of \"ν\" in two places (v⊨I(ℓ)∧g and v′ = v[Y]).","section":"Section 2.1"},{"comment":"Reference [9] has an incomplete DOI: \"doi:10.1007/978-3-540-7\" appears truncated and should be completed.","section":"References"},{"comment":"The abstract states the improvement is \"almost two orders of magnitude faster than the naive method,\" while Section 5 says Incl is \"more than one order of magnitude\" and Expand is \"almost another order\". Please state the speedup factors consistently and specify the exact measured values (e.g., geometric means or median speedups).","section":"Section 5 and Abstract"},{"comment":"The paper says Tiga can verify only a strict subset of TATL and compares on 150 of the 236 queries; it would be helpful to state explicitly which TATL constructs Tiga cannot handle (e.g., nested coalition quantifiers) and to clarify that the remaining 86 queries use those constructs.","section":"Section 5"},{"comment":"The cactus plots are hard to read without additional details: please indicate the number of queries, the per-query timeout, and the hardware/software environment used for the experiments.","section":"Figures 4 and 5"}],"recommendation":"major_revision","confidential_remarks":"The error in Eq. (4)/(6) is serious but appears fixable; the intended symbolic characterization is close to standard timed-game predecessor computations, and the experimental evaluation suggests the implementation uses a correct semantics. If the authors repair the symbolic equations, re-prove Lemma 9 and Theorem 10, and provide a rigorous proof of Theorem 18, the paper could be a strong contribution. I recommend major revision rather than rejection, provided the authors also clarify the relation between the prose and the symbolic definitions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper is worth reading but needs a serious fix. The genuinely new pieces—vertex merging as derivation (Theorem 14) and the expansion abstraction—are clean and plausible. The implementation story with Uppaal and the reproducibility package is a strong plus. If the encoding were right, this would be a solid contribution to on-the-fly timed verification.\n\nThe problem is the symbolic characterization of Forceable and Unavoidable. The prose definitions allow the system to stay in Wphi1 during the delay until Wphi2 is reached. Equations (4) and (6) instead put Wphi1 \\ Wphi2 into the avoid set of Predlambda, which forbids exactly those states. The stress-test counterexample is real: a single location with invariant x<=10, no actions, and phi = <<S>>(true U x>=5). From x=0 the coalition can just wait; the state satisfies the formula. But Forceable as written computes Predlambda([5,10],[0,5)) = [5,10], so x=0 is not included. The same inversion appears in Unavoidable. So Theorem 10 is false as stated, and Theorem 18 inherits the problem. The proof of Theorem 10 handwaves the until case, so the contradiction between prose and equation is not caught.\n\nThis is a load-bearing flaw, not a stylistic one. If the implementation follows the equations, the tool under-approximates until properties; if it follows the prose, the paper's formal definitions don't match the algorithm. Either way, a revision is necessary.\n\nOther soft spots are minor by comparison: Theorem 18 is sketched in two sentences, and the experimental claims would benefit from a few more methodological details (model sizes, timeouts, spread). The abstraction's practical premise—that most valuations are eventually reached—is stated but not deeply validated; on easy queries the extra edges do slow things down, as the paper admits.\n\nWho should read it: researchers building on-the-fly algorithms for timed multiplayer games, and anyone using EADG encodings. The vertex merging theorem and the abstraction idea have value beyond the buggy until case.\n\nRecommendation: send to peer review with a clear request for major revision. The authors need to correct Equations (4) and (6) to match their own prose, redo the proof of Theorem 10 properly, and then rerun the experiments. The rest of the structure is sound.","headline":"Useful TATL-on-EADG engineering with a real correctness bug in the symbolic until characterization.","tokens_in":23356,"tokens_out":4537,"would_cite":false,"duration_ms":51475,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A new algorithm verifies timed alternating-time temporal logic on the fly, and a zone-expansion abstraction makes it nearly an order of magnitude faster.","keywords":["timed alternating-time temporal logic","on-the-fly verification","extended abstract dependency graphs","vertex merging","inclusion checking","abstraction","timed multiplayer games","symbolic fixed point"],"falsifier":"On a benchmark family of timed games in which each location's invariant contains a large infeasible region whose outgoing edges are never enabled from any reachable valuation, compare the expansion abstraction with the inclusion-checking configuration: if the abstraction is not faster there, the near-order-of-magnitude performance claim is refuted. As a formal check, compute the zone-based fixed point on a small delay-closed example without abstraction and require the answers to agree with the abstracted algorithm for all TATL formulas considered.","tokens_in":22354,"feed_emoji":"⏱️","tokens_out":13229,"duration_ms":138446,"temperature":0.7,"pith_summary":"The paper develops an on-the-fly symbolic algorithm for verifying timed alternating-time temporal logic (TATL) on timed multiplayer games, where coalitions of players choose strategies and the logic supports nested coalition quantifiers and real-time constraints. The algorithm encodes the verification problem into extended abstract dependency graphs (EADGs), so that only the states and sub-formulas needed to answer the query are explored. The authors prove the encoding is sound and complete: on a delay-closed symbolic region $R$, the least fixed point of the generated graph equals the set of states in $R$ satisfying the formula. They then generalize inclusion checking to a vertex-merging operation and, building on it, introduce an expansion abstraction that replaces every symbolic zone by the full invariant zone of its location; this preserves correctness, removes the need for inclusion checks, and in experiments makes the verifier nearly an order of magnitude faster than previous tools on the same queries.","feed_headline":"Zone-expansion abstraction speeds timed multi-agent checks by ~10x","feed_subtitle":"On-the-fly dependency-graph algorithm plus invariant-zone abstraction verifies TATL properties faster than prior tools.","key_machinery":"The argument is carried by the extended abstract dependency graph (EADG) least-fixed-point computation: vertices $\\langle R,\\phi\\rangle$ carry value functions that combine the values of sub-formula vertices and action-successor vertices, and the fixed point over a Noetherian ordering of zone federations is computed on the fly. Two symbolic transformers, $\\mathit{Forceable}_S$ and $\\mathit{Unavoidable}_S$, form the semantic core: they decide from which valuations a coalition can force a state by delays and its own actions, and from which it cannot avoid one. The correctness identity is $\\alpha^G_{\\min}(\\langle R,\\phi\\rangle) = R \\cap \\llbracket\\phi\\rrbracket$ for delay-closed $R$, proved by induction and supported by the invariant that every generated region is closed under delay. The expansion abstraction $X(\\langle \\ell,Z,\\phi\\rangle)=\\langle \\ell,\\llbracket I(\\ell)\\rrbracket,\\phi\\rangle$ is the optimization that removes the need for inclusion checking while keeping the fixed point correct.","core_discovery":"At the heart of the paper is a correct encoding of TATL model checking into extended abstract dependency graphs (EADGs). Vertices are pairs $\\langle R,\\phi\\rangle$ of a symbolic state (a location and a zone) and a TATL formula; the assignment domain is a Noetherian ordering of zone federations, and each vertex's value function computes, from the answers to its dependencies, the subset of $R$ where $\\phi$ holds. Two workhorse transformers, $\\mathit{Forceable}_S$ and $\\mathit{Unavoidable}_S$, compute the sets of states from which coalition $S$ can force a move into a target set while staying inside a safety set, and from which $S$ cannot avoid such a move; these mirror the strategic and inevitable branches of TATL semantics. The paper proves by structural induction that for delay-closed $R$, the least fixed point $\\alpha^G_{\\min}(\\langle R,\\phi\\rangle)$ equals $R \\cap \\llbracket\\phi\\rrbracket$ (Theorem 10), making the encoding sound and complete. It then adds a general vertex-merging rule: if a monotone function $f$ maps the fixed-point value of a vertex $v_2$ to that of $v_1$, then $v_1$ can be removed and its dependents redirected through $f$ (Theorem 14), generalizing classical inclusion checking. Using this, the expansion abstraction $X(\\langle \\ell,Z,\\phi\\rangle)=\\langle \\ell,\\llbracket I(\\ell)\\rrbracket,\\phi\\rangle$ replaces every zone by the location's full invariant zone; the paper proves this preserves correctness (Theorem 18) and reports nearly an order-of-magnitude speedups in benchmarks.","pith_inferences":["A hybrid strategy that uses the full invariant zone only for locations where the reachable zone covers most of the invariant, and falls back to inclusion checking elsewhere, could retain the speedup while guarding against models with many useless edges.","The derivation/vertex-merge mechanism is generic: any domain with a Noetherian ordering and monotonically composable value functions can reuse it, so the idea should transfer to weighted or probabilistic variants of CTL and ATL.","The benchmark evidence suggests the abstraction's main cost appears on trivial queries, where extra edges delay early termination; a query-difficulty-aware scheduling heuristic could mitigate that cost independently of the abstraction itself."],"forward_implications":["TATL formulas with nested coalition quantifiers and freeze timing constraints can now be checked without precomputing the full state space, with early termination on both positive and negative answers.","The vertex-merging generalization makes inclusion checking available in any EADG-based analysis, and the paper points to Petri-net coverability checks as a natural next domain.","The expansion abstraction removes the need for inclusion checks in the timed-game setting altogether, so the per-query work concentrates on location-formula pairs rather than zone inclusions.","Because TATL subsumes TCTL, the result also supplies the first on-the-fly algorithm for TCTL with the generic freeze operator."],"supporting_citations":[{"why":"Supplies the extended abstract dependency graph framework and the on-the-fly fixed-point algorithm the encoding extends.","marker":"[18]"},{"why":"Provides the safe timed-predecessor operators, the unsatisfied-encoding trick, and the earlier on-the-fly timed-game algorithm that this work generalizes.","marker":"[13]"},{"why":"Shows how ATL verification is encoded into EADGs in the untimed case, which this paper extends to timed games and TATL.","marker":"[12]"},{"why":"Defines alternating-time temporal logic, whose timed extension is the object of study.","marker":"[4]"},{"why":"Gives the zone and difference-bound-matrix operations used by all symbolic value functions.","marker":"[10]"},{"why":"Supplies the timed until semantics detail (the disjunction in big-step runs) that the Forceable and Unavoidable transformers reflect.","marker":"[5]"},{"why":"Introduces abstract dependency graphs and their application to model checking, the foundation of the EADG setup.","marker":"[17]"},{"why":"Justifies the bounded-clock assumption that keeps the symbolic dependency graph finite.","marker":"[8]"}],"fun_headline_variants":["Zone-expansion abstraction makes timed multi-agent checks ~10x faster","On-the-fly TATL verification with abstraction yields 10x speedup","New abstraction accelerates timed strategy verification by 10x","Timed ATL checks get 10x boost from zone-expansion trick"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The practical speed advantage of the expansion abstraction rests on the belief that in most timed automata nearly every edge out of a location is eventually usable, so enlarging each symbolic zone to the location's full invariant adds little irrelevant work.","fun_headline_variants_meta":{"raw":{"variants":["Zone-expansion abstraction makes timed multi-agent checks ~10x faster","On-the-fly TATL verification with abstraction yields 10x speedup","New abstraction accelerates timed strategy verification by 10x","Timed ATL checks get 10x boost from zone-expansion trick"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000493,"raw_usage":{"total_tokens":2510,"prompt_tokens":1121,"completion_tokens":1389,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":737,"completion_tokens_details":{"reasoning_tokens":1312}},"tokens_in":737,"tokens_out":1389,"duration_ms":12238,"temperature":1.0,"reasoning_tokens":1312,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:23:07.372278+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"On a benchmark family of timed games in which each location's invariant contains a large infeasible region whose outgoing edges are never enabled from any reachable valuation, compare the expansion abstraction with the inclusion-checking configuration: if the abstraction is not faster there, the near-order-of-magnitude performance claim is refuted. As a formal check, compute the zone-based fixed point on a small delay-closed example without abstraction and require the answers to agree with the abstracted algorithm for all TATL formulas considered.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows how ATL verification is encoded into EADGs in the untimed case, which this paper extends to timed games and TATL."}],"review_version":1}