Antichains for Concurrent Parameterized Games

Ga\"etan Staquet; Nathalie Bertrand; Patricia Bouyer

REVIEW 2 major objections 3 minor 13 references

Antichains for Concurrent Parameterized Games

T0 review · 2 major / 3 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2505.13460 v2 pith:E2RFUT44 submitted 2025-05-02 cs.LO cs.GT

Nathalie Bertrand , Patricia Bouyer , Gaëtan Staquet This is my paper · ORCID

classification cs.LOcs.GT

keywords concurrentgamesparameterizedverificationantichainsknowledgegamereachabilityfixed-pointalgorithmssymboliccomputation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

The 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.

Now the soft spots, in order of importance.

First, 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.

Second, 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.

Smaller 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.

The 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.

Who 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.

Referee Report

2 major / 3 minor

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.

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 (2)

[Theorem 22 / Definition 12] 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 3.2] 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.

minor comments (3)

[Appendix A.3, Lemma 23] The notation J1,nK is used without definition; please define it (presumably the set of successors of the relevant vertex).
[Example 13] In the displayed W0, a comma is missing between (x2,∅) and (y1,∅).
[Definition 12] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the fixed-point characterization and both antichain algorithms are derived and proved from the knowledge-game semantics, with no fitted parameters or output-dependent premises.

full rationale

The paper's derivation chain is self-contained for its central claim. The antichain fixed point (Definition 12) is defined directly from the predecessor structure of the knowledge game, and Theorem 14 proves, by a standard two-sided attractor induction, that the downward closure of the accumulated antichain equals Eve's winning region for every nonempty knowledge set. The proof in Appendix A.2 constructs winning strategies from W_i and conversely extracts membership in W_i from a winning strategy; neither direction imports the theorem it is proving. The equality of the three algorithms (Theorem 21) is established through operator inclusions (Lemma 23) and finite stabilization of the A-coherent lattice K_A, again without assuming the desired conclusion. The knowledge-game equivalence (Theorem 6) and PSPACE-completeness (Theorem 4) are cited from the authors' previous paper [2], but those are independent published theorems with stated assumptions that do not include the present paper's results; they are load-bearing for the application to the original parameterized game, but they are not circular because they are not derived from, or equivalent to, the new antichain output. There is no data fitting, no parameter calibrated to a subset of the benchmark outcomes, and no 'prediction' that is in fact a renamed input. Two correctness-level caveats, which are not circularity, should be noted: the monotonicity observation in Section 3.2 is asserted without proof (it is intuitively true and compatible with the fixed-point proof, but it is a missing argument), and Theorem 22 is stated for all maximal elements whereas Theorem 14 explicitly restricts to K ≠ ∅; depending on the deadlock convention for (v,∅) vertices, the literal 'maximal elements of the winning region' wording may over-approximate. Neither caveat is a reduction of the derivation to its own inputs, so the circularity score remains 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The algorithms contain no fitted constants and no invented entities. The paper depends on standard lattice and game-theoretic background, on the explicit completeness assumption in Definition 1, on the finiteness of the generated lattice for the chosen representation of constraints, and on the knowledge-game equivalence theorem from the authors' earlier work [2]. These are all stated or cited, and none of them is calibrated to make the target result come out.

assumptions (5)

standard math Turn-based reachability games admit memoryless winning strategies for the reachability player.
Used in the proof of Theorem 14 (Appendix A.2) to assume Eve's winning strategy in KnowG is memoryless; cited to [10].
standard math König's lemma: an infinite finitely branching tree has an infinite branch.
Used implicitly in the proof of Theorem 14 to conclude that the tree of all plays under a winning memoryless strategy is finite because every branch is finite.
domain assumption The arena is complete for enabled actions: if action a is enabled at v, then Δ(v,a,k) is nonempty for all k>0.
Part of Definition 1; ensures the decomposition identity (2) holds, which is used in the proof of Lemma 23 and in the WAlt algorithm.
domain assumption Each ∇(v,a,v') is a finite union of intervals for the implementation; the theory assumes only effective union, intersection, and difference operations.
Guarantees the A-coherent lattice KA is finite and the algorithms terminate; stated in Section 2.1 and used throughout the implementation in Section 4.
domain assumption The knowledge-game equivalence: Eve wins in the parameterized game from v if and only if she wins from (v,N>0) in KnowG (Theorem 6 of [2]).
Cited from the authors' earlier work; transfers the computed knowledge-game winning region back to the original parameterized game in Corollary 16.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Antichains for Concurrent Parameterized Games." pith.science (2026). https://pith.science/paper/E2RFUT44

@misc{pith2026250513460,
  author       = {Pith},
  title        = {Pith review of: Antichains for Concurrent Parameterized Games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/E2RFUT44}},
  note         = {Machine review of arXiv:2505.13460}
}

read the original abstract

Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n). Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE-membership proof is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents. In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented these two algorithms in C++, as well as the one initially proposed, and report on their relative performances on various benchmarks.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

13 extracted references · 9 canonical work pages

[1]

Krzysztof Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters , 22(6):307--309, May 1986. https://doi.org/10.1016/0020-0190(86)90071-2 doi:10.1016/0020-0190(86)90071-2

doi:10.1016/0020-0190(86)90071-2 1986
[2]

C oncurrent P arameterized G ames

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. C oncurrent P arameterized G ames. In Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, ( FSTTCS '19) , volume 150 of LIPIcs , pages 31:1--31:15. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2019. https://doi.org/10.42...

work page doi:10.4230/lipics.fsttcs.2019.31 2019
[3]

Antichain-based qbf solving

Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin. Antichain-based qbf solving. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11) , volume 6996 of Lecture Notes in Computer Science , pages 183--197. Springer

work page
[4]

P \' e rez

Micha \" e l Cadilhac and Guillermo A. P \' e rez. Acacia-bonsai: A modern implementation of downset-based LTL realizability. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ( TACAS '23) , volume 13994 of Lecture Notes in Computer Science , pages 192--207. Springer, 2023. https://doi...

doi:10.1007/978-3-031-30820-8 2023
[5]

Henzinger, and Jean-François Raskin

Martin De Wulf , Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Antichains: a new algorithm for checking universality of finite automata. In Proceedings of the 18th International Conference on Computer-Aided Verification (CAV'06) , volume 4144 of Lecture Notes in Computer Science , pages 17--30. Springer, 2006

work page 2006
[6]

A lattice theory for solving games of imperfect information

Martin De Wulf , Laurent Doyen, and Jean-François Raskin. A lattice theory for solving games of imperfect information. In Proceedings of 9th International Workshop on Hybrid Systems: Computation and Control (HSCC'06) , volume 3927 of Lecture Notes in Computer Science , pages 153--168. Springer, 2006

work page 2006
[7]

Antichains for the automata-based approach to model-checking

Laurent Doyen and Jean-François Raskin. Antichains for the automata-based approach to model-checking. Logical Methods in Computer Science , 5(1), 2009

work page 2009
[8]

Antichains algorithms for finite automata

Laurent Doyen and Jean-François Raskin. Antichains algorithms for finite automata. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10) , volume 6015 of Lecture Notes in Computer Science , pages 2--22. Springer, 2010

work page 2010

Show all 13 references

[9]

Keeping a crowd safe: On the complexity of parameterized verification (invited talk)

Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS '14) , volume 25 of LIPIcs , pages 1--10. Schloss Dagstuhl - Leibniz-Zentr...

doi
[10]

Games on Graphs

Nathana \" e l Fijalkow, Nathalie Bertrand, Patricia Bouyer - Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen - Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotn \' y , Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivie...

2023 doi arXiv
[11]

An antichain algorithm for LTL realizability

Emmanuel Filiot, Naiyong Jin, and Jean-Fran c ois Raskin. An antichain algorithm for LTL realizability. In P roceedings of the 21st I nternational C onference on C omputer A ided V erification ( CAV '09) , volume 5643 of Lecture Notes in Computer Science , pages 263--277. Spri...

2009
[12]

German and A

Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. Journal of the ACM , 39(3):675--735, July 1992. https://doi.org/10.1145/146637.146681 doi:10.1145/146637.146681

1992
[13]

Antichains: alternative algorithms for LTL satisfiability and model-checking

Martin De Wulf, Laurent Doyen, Nicolas Maquet, and Jean-François Raskin. Antichains: alternative algorithms for LTL satisfiability and model-checking. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACA...

2008

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [1]

Krzysztof Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters , 22(6):307--309, May 1986. https://doi.org/10.1016/0020-0190(86)90071-2 doi:10.1016/0020-0190(86)90071-2

doi:10.1016/0020-0190(86)90071-2 1986

[2] [2]

C oncurrent P arameterized G ames

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. C oncurrent P arameterized G ames. In Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, ( FSTTCS '19) , volume 150 of LIPIcs , pages 31:1--31:15. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2019. https://doi.org/10.42...

work page doi:10.4230/lipics.fsttcs.2019.31 2019

[3] [3]

Antichain-based qbf solving

Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin. Antichain-based qbf solving. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11) , volume 6996 of Lecture Notes in Computer Science , pages 183--197. Springer

work page

[4] [4]

P \' e rez

Micha \" e l Cadilhac and Guillermo A. P \' e rez. Acacia-bonsai: A modern implementation of downset-based LTL realizability. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ( TACAS '23) , volume 13994 of Lecture Notes in Computer Science , pages 192--207. Springer, 2023. https://doi...

doi:10.1007/978-3-031-30820-8 2023

[5] [5]

Henzinger, and Jean-François Raskin

Martin De Wulf , Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Antichains: a new algorithm for checking universality of finite automata. In Proceedings of the 18th International Conference on Computer-Aided Verification (CAV'06) , volume 4144 of Lecture Notes in Computer Science , pages 17--30. Springer, 2006

work page 2006

[6] [6]

A lattice theory for solving games of imperfect information

Martin De Wulf , Laurent Doyen, and Jean-François Raskin. A lattice theory for solving games of imperfect information. In Proceedings of 9th International Workshop on Hybrid Systems: Computation and Control (HSCC'06) , volume 3927 of Lecture Notes in Computer Science , pages 153--168. Springer, 2006

work page 2006

[7] [7]

Antichains for the automata-based approach to model-checking

Laurent Doyen and Jean-François Raskin. Antichains for the automata-based approach to model-checking. Logical Methods in Computer Science , 5(1), 2009

work page 2009

[8] [8]

Antichains algorithms for finite automata

Laurent Doyen and Jean-François Raskin. Antichains algorithms for finite automata. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10) , volume 6015 of Lecture Notes in Computer Science , pages 2--22. Springer, 2010

work page 2010