{"id":"32c5af5e-d022-4dc3-9b89-e087db1a3525","arxiv_id":"2505.13460","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Two fixed-point algorithms over antichains compute Eve's winning region in concurrent parameterized reachability games, with proofs of correctness and a C++ implementation.","lead":"The paper introduces two antichain-based fixed-point algorithms that compute the winning region for a player in concurrent parameterized reachability games, where the number of opponents is unknown. The algorithms are proven correct, implemented in C++, and benchmarked against the previous DFS method on synthetic and QBF-derived games.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 22 overstates correctness: the antichain W∞ includes losing bottom elements (v,∅), so it is not exactly the maximal elements of the winning region.","rationale":"The reader identified downward-closedness as the weakest assumption, but that property is actually a consequence of Theorem 14 and is not the critical gap. The more serious issue is that W0 seeds the antichain with (v,∅) for all non-target vertices, and these losing bottom elements survive in W∞ for vertices with no winning nonempty knowledge. This makes Theorem 22 literally false, as the antichain contains elements outside the winning region. The impact is contained: the decision procedure (Corollary 16) and the fixed-point characterization for nonempty K are unaffected, and the fix is straightforward—either filter out ∅-knowledge sets from the final antichain or restate Theorem 22 with an explicit caveat. Because the main theorem as written is central to the paper's contribution and needs a correction, the appropriate verdict is conditional acceptance, additionally requiring the experimental reproducibility fixes already noted by the reader. I do not see a substantive issue with the algorithmic convergence or the equivalence theorems; the concern is a precise but fixable over-approximation in the statement of the main result.","tokens_in":20922,"tokens_out":45468,"duration_ms":434355,"concrete_test":"Run ParaGraphs on the minimal arena V={v,s,t} with target t, a single action a from v to s for all k, and no outgoing edges from s (or a self-loop at s). Eve cannot win from any nonempty K at v. The algorithm's output antichain should contain (v,∅) and (s,∅) alongside (t,N>0). Check that (v,∅) is present; since from (v,∅) the play is stuck at (v,∅,a) and never reaches t, it is losing. If (v,∅) appears in W∞, then W∞ is not the set of maximal winning vertices, confirming the flaw in Theorem 22.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim, Theorem 22, states that W∞ describes the maximal elements of Eve's winning region in KnowG. However, the fixed-point initialization W0 includes (v,∅) for every v∈V\\{t} (Definition 12). These elements are never removed unless a nonempty knowledge set at the same v is later added to the antichain. For any vertex v where Eve has no winning strategy with nonempty knowledge, (v,∅) remains in W∞. But from (v,∅), any action leads to an Adam vertex (v,∅,a) with no outgoing edges because ∅∩∇(v,a,v′) = ∅ for all v′; the play is stuck and never reaches a target, so (v,∅) is losing. Thus W∞ contains losing vertices, and the winning region's maximal elements are a proper subset of W∞. The proof of Theorem 22 passes through Theorem 14, which explicitly restricts to K≠∅; the empty-knowledge elements are outside its scope. Consequently, the statement 'describes the maximal elements of the winning region' is false unless one either removes all (v,∅) from the output or explicitly declares that the empty knowledge set is a sentinel for 'no winning knowledge' rather than a winning vertex. The algorithms remain correct for the decision problem (Corollary 16) and for all nonempty knowledge sets, but the headline theoretical claim over-approximates the winning region.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes antichain-based symbolic algorithms for computing Eve's winning region in the knowledge game associated with concurrent parameterized reachability games. It gives a least-fixed-point characterization of the winning region via an operator on antichains of knowledge sets (Definition 12), an alternative \"operational\" fixed-point iteration (Definition 17), and proves that the two schemes coincide (Theorem 21). The paper then claims that the resulting antichain describes the maximal elements of Eve's winning region (Theorem 22), and reports on a C++ implementation of both new algorithms and the earlier DFS algorithm, with benchmarks on synthetic arenas and QBF-derived instances.","tokens_in":21148,"tokens_out":11076,"duration_ms":117899,"significance":"If repaired, this is a useful contribution: it is, to my knowledge, the first symbolic computation of the full winning region for concurrent parameterized reachability games, rather than merely a decision procedure for a given initial vertex. The equivalence proof between the two fixed-point schemes is nontrivial and the appendix gives detailed arguments. The paper also ships an open-source implementation and a reasonably extensive experimental comparison. The derivations are parameter-free and the main proof obligations are checkable. However, the central correctness claim is currently overstated because the output antichain contains losing empty-knowledge sentinel vertices.","major_comments":[{"comment":"The statement that W∞ describes the maximal elements of Eve's winning region in KnowG is false as written. The initialization W0 in Definition 12 contains (v,∅) for every v∈V\\{t}, and these vertices are never removed unless a nonempty knowledge set at the same vertex is later added to the antichain. For any vertex v with no winning nonempty knowledge, (v,∅) therefore remains in W∞. But (v,∅) is losing: from the Eve vertex (v,∅), every Adam successor is (v,∅,a), and since ∅∩∇(v,a,v′)=∅ for all v′, that Adam vertex has no outgoing edge, so the play is stuck and never reaches t. For example, (s,∅) remains in W∞ for the arena of Figure 1 and is losing. Consequently Theorem 22 does not follow from Theorem 14, which explicitly restricts to K≠∅. Please either remove all sentinel elements (v,∅) with v≠t from the output, or restate Theorem 22 as \"W∞ together with the losing sentinel (v,∅) encodes the winning region\", and adjust the abstract and Section 1 accordingly. Corollary 16, which only queries (v0,N>0), is unaffected.","section":"Theorem 22 / Definition 12"},{"comment":"The antichain representation rests on the assertion, stated without proof, that Eve's winning region in KnowG is downward-closed: if Eve wins from (v,K), then she wins from (v,K′) for every K′⊆K. This monotonicity is load-bearing: if it failed, keeping only maximal knowledge sets would not represent the winning region and both algorithms would be unsound. The claim is plausible, but it should be proved or given an explicit reference. A proof can be obtained by transferring a memoryless winning strategy from (v,K) and observing inductively that the knowledge along every play from (v,K′) remains a subset of the knowledge along the corresponding play from (v,K). Please add such a proof.","section":"Section 3.2"}],"minor_comments":[{"comment":"The notation J1,nK is used without definition; please define it (presumably the set of successors of the relevant vertex).","section":"Appendix A.3, Lemma 23"},{"comment":"In the displayed W0, a comma is missing between (x2,∅) and (y1,∅).","section":"Example 13"},{"comment":"The parenthetical \"(v,∅) represents that a priori Eve loses against any number of players from v\" is a sentinel convention, not a statement that (v,∅) is winning; this should be made explicit at the definition site so that Theorem 22 is not read as claiming W∞⊆WinningRegion.","section":"Definition 12"}],"recommendation":"major_revision","confidential_remarks":"The empty-knowledge sentinel issue is real but localized and fixable within the manuscript's scope; I would not reject over it. The paper relies appropriately on the authors' earlier work [2] for the knowledge-game equivalence and PSPACE-completeness. I would ask for a revised version in which Theorem 22 and the abstract are corrected and the downward-closure proof is supplied."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe core of the paper is solid and novel. For concurrent parameterized reachability games, the authors give the first algorithms that compute the full winning region in the knowledge game as an antichain, rather than just deciding a single initial vertex. The fixed-point characterization (Thm 14), the two iterative schemes (Def 12 and 17), and the equivalence proof (Thm 21) are nontrivial; I went through the appendix and the inclusions in Lemma 23 check out. The implementation is open source, and the experiments honestly report that antichains are not uniformly faster than the existing DFS—that kind of reporting earns credit.\n\nNow the soft spots, in order of importance.\n\nFirst, Theorem 22 as stated is false. The antichain W∞ includes (v,∅) for every non-target v, and these states are never removed. But (v,∅) is losing in KnowG: any Adam successor (v,∅,a) has no outgoing edges. So W∞ is not the set of maximal elements of the winning region; it is the winning region's maximal nonempty elements plus those losing bottom markers. The proof of Theorem 22 invokes Theorem 14, which only covers K≠∅, so the gap is real. The repair is easy—filter out (v,∅) from the output or explicitly call them sentinels for 'no winning knowledge'—but the current wording overclaims.\n\nSecond, the QBF benchmarks are not reproducible. Formulas are 'randomly generated' with no seeds and no concrete instances. Given the paper's honest experiments, this is a fixable deficiency: release the instances or a seeded generator and a commit hash for ParaGraphs.\n\nSmaller point: the downward-closedness observation, on which the whole antichain representation rests, is stated without proof. It is true, and a short proof would settle it.\n\nThe reliance on the authors' own prior results (Theorem 6 and PSPACE-completeness) is acceptable; those are established theorems. I see no circularity or fitted parameters.\n\nWho is this for? Researchers in parameterized verification and antichain methods for games. It deserves a serious referee. I'd recommend acceptance after a revision that corrects Theorem 22 and provides reproducible QBF data.","headline":"The antichain algorithms are a genuine advance and the core proofs check out, but Theorem 22 overstates the result by counting losing empty-knowledge states as winning, and the QBF benchmarks lack reproducibility.","tokens_in":21730,"tokens_out":4357,"would_cite":true,"duration_ms":42129,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that Eve's winning region in a concurrent parameterized reachability game can be represented as an antichain of maximal knowledge sets, and that two fixed-point algorithms compute it exactly.","keywords":["concurrent games","parameterized verification","antichains","knowledge game","reachability games","fixed-point algorithms","symbolic computation"],"falsifier":"Construct any finite parameterized arena and exhaustively enumerate the true winning region of the knowledge game; if some state $(v,K)$ is winning while a strict subset $K'\\subset K$ is losing, the downward-closure premise is false and both antichain algorithms would misreport the region. A concrete search over small arenas for such a violating state would settle the central claim.","tokens_in":20682,"feed_emoji":"🎮","tokens_out":6144,"duration_ms":59559,"temperature":0.7,"pith_summary":"Concurrent parameterized games pit one player, Eve, against an unknown number of opponents, and previous work reduced her reachability objective to a two-player 'knowledge game' whose state space is exponential. This paper tries to show that the winning region of that knowledge game has a compact symbolic shape: because winning with a coarse knowledge set implies winning with every finer one, the whole region is captured by its maximal knowledge sets, an antichain. It proves that two fixed-point algorithms—one iterating over a finite lattice of relevant knowledge sets, one constructing knowledge sets operationally—compute exactly those maximal elements and hence the minimal knowledge Eve needs at every vertex. The authors also implement all three algorithms and compare running times on synthetic and QBF-derived arenas.","feed_headline":"Antichains compute full winning regions in parameterized games","feed_subtitle":"Two fixed-point algorithms store only maximal knowledge sets, giving the minimal information Eve needs to win.","key_machinery":"The load-bearing object is the antichain of maximal knowledge sets on the partial order where $(v,K) \\sqsubseteq (v,K')$ iff $K \\subseteq K'$, taken over the finite A-coherent lattice $\\mathcal{K}_A$ generated by the edge constraints. The key identity is that the constrained-predecessor operator $\\mathrm{KPred}[v,a](S)$ and its operational variant $\\mathrm{KPredAlt}[v,a](S)$ agree on downward-closed sets, and their iterates coincide at every step; this lets a fixed point over a finite lattice certify the full-lattice computation. The monotonicity observation that Eve wins from a knowledge set whenever she wins from every subset is what justifies storing only maximal elements as an antichain.","core_discovery":"The central claim is Theorem 22: the antichains $W^\\infty$, $W^\\infty_\\mathrm{Alt}$, and $W^\\infty_{\\mathcal{K}}$ are exactly the maximal elements of Eve's winning region in the knowledge game $\\mathrm{KnowG}$. On the paper's own terms, this means the exponential-size knowledge game does not need to be explored state by state. Because the region is downward-closed under knowledge inclusion, storing only maximal knowledge sets loses nothing, and both proposed fixed-point schemes converge to the same representation that the original PSPACE algorithm could only query pointwise. Through the known reduction, Eve wins the parameterized game from a vertex $v$ exactly when $(v,\\mathbb{N}_{>0})$ belongs to the computed antichain.","pith_inferences":["Beyond the paper's own claims, the same antichain machinery should transfer to safety or parity objectives in concurrent parameterized games, provided the least fixed point remains monotone under knowledge refinement; the paper does not discuss this.","The QBF-based benchmark construction suggests a practical line the authors do not pursue: the lattice-construction routine is fast enough that a standalone antichain-based QBF checker built from this reduction is worth testing.","A hybrid algorithm that runs the pointwise DFS first and switches to antichains when a full region is requested would combine the strengths reported in the experiments; the paper leaves algorithm choice as future work."],"forward_implications":["Eve's decision problem can be answered by checking $(v,\\mathbb{N}_{>0})$ against the computed antichain, avoiding a state-by-state DFS over the exponential knowledge game.","The two fixed-point algorithms produce the full winning region, so the minimal knowledge Eve needs at every vertex is available, not just a yes/no answer.","The two characterizations are provably equivalent, and the finite coherent lattice makes termination immediate.","The symbolic formulation works for any edge-label family with effective union, intersection, and difference operations, not only finite unions of intervals.","On the reported benchmarks the antichain algorithms can outperform the original DFS on negative instances, while the DFS remains faster on many positive instances."],"supporting_citations":[{"why":"Supplies the concurrent parameterized game model, the reduction to the knowledge game, the PSPACE-completeness result, and the QBF hardness construction used in benchmarks.","marker":"[2]"},{"why":"Supplies the lattice and antichain theory, including join, meet, domination, and downward-closure operations, that the paper adapts to knowledge sets.","marker":"[6]"},{"why":"Supplies the standard theory of two-player turn-based reachability games used in the fixed-point correctness proof and attractor computations.","marker":"[10]"}],"fun_headline_variants":["Antichains shrink parameterized games to minimal knowledge","Full winning regions via antichains in parameterized games","Two fixed-point algorithms with antichains beat state-by-state","Antichain fixed points yield Eve's minimal winning knowledge","Symbolic antichains: minimal knowledge to win parameterized games"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything rests on the monotonicity claim, stated without proof, that if Eve wins with a given knowledge set she also wins with any smaller knowledge set; if that fails, the antichain of maximal sets no longer represents the winning region.","fun_headline_variants_meta":{"raw":{"variants":["Antichains shrink parameterized games to minimal knowledge","Full winning regions via antichains in parameterized games","Two fixed-point algorithms with antichains beat state-by-state","Antichain fixed points yield Eve's minimal winning knowledge","Symbolic antichains: minimal knowledge to win parameterized games"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000482,"raw_usage":{"total_tokens":2366,"prompt_tokens":912,"completion_tokens":1454,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":528,"completion_tokens_details":{"reasoning_tokens":1385}},"tokens_in":528,"tokens_out":1454,"duration_ms":10831,"temperature":1.0,"reasoning_tokens":1385,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:22:29.973496+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct any finite parameterized arena and exhaustively enumerate the true winning region of the knowledge game; if some state $(v,K)$ is winning while a strict subset $K'\\subset K$ is losing, the downward-closure premise is false and both antichain algorithms would misreport the region. A concrete search over small arenas for such a violating state would settle the central claim.","supporting_citations":[{"cited_title":"C oncurrent P arameterized G ames","cited_arxiv_id":null,"evidence_quote":"Supplies the concurrent parameterized game model, the reduction to the knowledge game, the PSPACE-completeness result, and the QBF hardness construction used in benchmarks."},{"cited_title":"A lattice theory for solving games of imperfect information","cited_arxiv_id":null,"evidence_quote":"Supplies the lattice and antichain theory, including join, meet, domination, and downward-closure operations, that the paper adapts to knowledge sets."}],"review_version":1}