arxiv: 2604.22648 · v1 · submitted 2026-04-24 · 💻 cs.FL

Recognition: unknown

An algebraic characterisation of Eve-positional languages

Olivier Idir, Thomas Colcombet

Pith reviewed 2026-05-08 08:37 UTC · model grok-4.3

classification 💻 cs.FL

keywords Eve-positionalityomega-regular languagesalgebraic characterisationmemoryless strategiesgames on graphsautomata theorysynthesisverification

0 comments

The pith

ω-regular languages are Eve-positional exactly when they satisfy a short list of local algebraic properties.

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

The paper establishes an algebraic characterisation of Eve-positionality for ω-regular languages: the property holds precisely when a small number of elementary local conditions are met in the language's algebraic structure. Eve-positionality means that in any game whose winning condition is membership in the language, the existential player has an optimal strategy that depends only on the current state and requires no memory of prior moves. This reduces a global strategic property to local checks, which matters because it simplifies the design of winning strategies in verification and controller synthesis tasks. The result is obtained by verifying the local properties after applying a reduction from two-player games to one-player arenas.

Core claim

An ω-regular language is Eve-positional if and only if a limited collection of elementary local algebraic properties hold. These properties are defined directly on the algebraic object associated with the language, and the equivalence is shown by first reducing the two-player setting to the one-player setting and then confirming that the local conditions are necessary and sufficient in that simpler case.

What carries the argument

The algebraic structure of the ω-regular language, together with a finite set of elementary local properties that must be checked on it.

If this is right

Eve possesses memoryless optimal strategies whenever the language satisfies the local conditions.
Positionality reduces to a finite, local verification task instead of an exhaustive search over game histories.
The same local conditions suffice for all two-player games once they hold in one-player arenas.
Controller synthesis for such languages can proceed with finite-state, history-free automata.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The local conditions could be turned into a decision procedure that runs directly on an automaton recognising the language.
Similar characterisations might exist for other memory requirements or for parity games with different player roles.
The approach suggests that many global game-theoretic properties of ω-regular objectives can be localised to algebraic identities.

Load-bearing premise

Positionality for Eve in all finite one-player arenas is sufficient to guarantee positionality in all two-player arenas.

What would settle it

An ω-regular language that meets every listed local algebraic property yet admits some two-player game in which every winning strategy for Eve must remember at least one bit of history.

read the original abstract

We present a new algebraic characterisation of Eve-positionality for $\omega$-regular languages. It involves only a limited number of elementary local properties to be checked. An $\omega$-regular language is Eve-positional if, in all games with this language as objective, the existential player (Eve) can play optimally without keeping any information concerning the history of the moves seen so far. This notion plays a crucial role in verification, automata theory and synthesis. Our proof heavily relies on a recent result of Casares and Ohlmann which states several characterisations of Eve-positionality for $\omega$-regular languages. More precisely, it relies on their a 1-to-2 player lift result: for an $\omega$-regular language, being Eve-positionally over all finite Eve-only arenas suffices for being Eve-positional over all two-player arenas.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper supplies a new algebraic characterisation of Eve-positionality for omega-regular languages via a short list of local properties, but the whole claim rests on the Casares-Ohlmann 1-to-2-player lift without an independent check.

read the letter

The main thing to know is that the authors give a characterisation of Eve-positional omega-regular languages that reduces to checking a limited number of elementary local properties on the syntactic semigroup. They obtain this by building directly on the Casares-Ohlmann result that positionality over finite Eve-only arenas lifts to all two-player arenas. The abstract is explicit that the new test is algebraic and local rather than a global game condition. That is the concrete advance they are offering. The paper does well in keeping the stated properties simple and in crediting the prior lift result instead of trying to reprove everything. Reusing recent work this way avoids unnecessary length and focuses attention on the local identities that supposedly suffice. If those identities are indeed easy to verify in practice, the characterisation could be useful for people who already compute syntactic semigroups in verification tools. The soft spot is the dependence on the external lift. The proof invokes it to move from Eve-only arenas to the general case, but does not contain a separate argument showing that the new local properties preserve the lift or that no counter-example arises inside this subclass. If the lift fails to apply exactly when the semigroup satisfies the listed identities, the characterisation does not fully carry over to two-player games. This is a real but contained limitation rather than a contradiction inside the paper itself. No circular definitions or invented entities appear in the description. The work is aimed at specialists in automata theory and infinite games who already know the positionality literature. A reader who follows algebraic approaches to omega-regular objectives will see immediate value in the local test and may cite the characterisation for its simplicity. It deserves a serious referee because the claim is specific, the reliance on prior work is stated clearly, and the result is falsifiable once the local properties are written out. I would send it to peer review.

Referee Report

1 major / 0 minor

Summary. The manuscript presents a new algebraic characterisation of Eve-positionality for ω-regular languages. It claims that such a language is Eve-positional precisely when its syntactic semigroup satisfies a finite collection of elementary local properties. The argument proceeds by reducing the general two-player case to Eve-only arenas via the 1-to-2-player lift theorem of Casares and Ohlmann, then verifying the local properties on the Eve-only side.

Significance. If the central claim is established, the result supplies a practical, finite algebraic test for Eve-positionality that can be checked directly on the syntactic semigroup. This would be useful for verification, synthesis, and automata-theoretic decision procedures, and it extends the recent characterisations of Casares and Ohlmann by isolating a small set of local identities.

major comments (1)

[Proof of the main theorem / application of the lift result] The proof of the main characterisation (invoked in the abstract and detailed in the body) rests entirely on the Casares–Ohlmann 1-to-2-player lift without an independent argument or verification that the listed local properties are preserved or sufficient under that lift. If the lift fails to transfer exactly to the semigroups satisfying the new identities, the claimed equivalence for two-player arenas does not hold.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and insightful comments. We address the major concern regarding the proof of the main theorem and the application of the lift result below.

read point-by-point responses

Referee: The proof of the main characterisation (invoked in the abstract and detailed in the body) rests entirely on the Casares–Ohlmann 1-to-2-player lift without an independent argument or verification that the listed local properties are preserved or sufficient under that lift. If the lift fails to transfer exactly to the semigroups satisfying the new identities, the claimed equivalence for two-player arenas does not hold.

Authors: We thank the referee for this observation. The 1-to-2-player lift theorem of Casares and Ohlmann establishes that, for any ω-regular language, Eve-positionality over all finite Eve-only arenas suffices to guarantee Eve-positionality over all two-player arenas. Our main result characterises Eve-positionality over Eve-only arenas precisely by the listed finite set of local identities on the syntactic semigroup. Since the syntactic semigroup is an invariant of the language, satisfaction of these identities is equivalent to the language being Eve-positional on Eve-only arenas; the lift theorem then applies directly at the language level to yield the two-player result. No additional preservation argument for the identities themselves is needed, as the lift does not act on the semigroup identities. To make this composition fully explicit, we will insert a clarifying paragraph immediately after the statement of the main theorem in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No circularity; new characterisation derived from external lift

full rationale

The manuscript explicitly attributes its core transfer from Eve-only arenas to two-player arenas to the external Casares-Ohlmann 1-to-2-player lift result, whose authors are distinct from Colcombet and Idir. The algebraic characterisation itself (finite local identities on the syntactic semigroup) is presented as the novel contribution obtained by direct inspection of Eve-only arenas; no equation, definition, or prediction inside the paper is shown to reduce by construction to another equation or fitted parameter of the same paper. No self-citation load-bearing, self-definitional loop, or renaming of a known result occurs. The derivation chain therefore remains non-circular even though it is not fully self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on the abstract, no free parameters, invented entities, or non-standard axioms are visible; the work operates inside the standard framework of ω-regular languages and two-player games on arenas.

axioms (2)

standard math ω-regular languages are closed under the usual Boolean operations and can be recognised by automata on infinite words
Implicit background for any algebraic characterisation in this domain.
domain assumption The 1-to-2 player lift result of Casares and Ohlmann holds for ω-regular objectives
Explicitly invoked in the abstract as the foundation of the proof.

pith-pipeline@v0.9.0 · 5433 in / 1289 out tokens · 42917 ms · 2026-05-08T08:37:03.678437+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

8 extracted references · 7 canonical work pages

[1]

Half-Positional Objectives Recognized by Deterministic Büchi Automata

1 Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors,33rd International Conference on Concurrency Theory (CON- CUR 2022), volume 243 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 20:...

2022
[2]

URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.20, doi:10.4230/LIPIcs.CONCUR.2022.20

Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.20, doi:10.4230/LIPIcs.CONCUR.2022.20. 2 J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies.Transactions of the American Mathematical Society, 138:295–311,

work page doi:10.4230/lipics.concur.2022.20 2022
[3]

3 Antonio Casares and Pierre Ohlmann

URL: http://www.jstor.org/stable/1994916. 3 Antonio Casares and Pierre Ohlmann. Positionalω-regular languages. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors,Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 21:1–21:14. ACM, 2024.doi:10.1145/3661814.3662087. ...

work page doi:10.1145/3661814.3662087 2024
[4]

URL:https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.FSTTCS.2014.379,doi:10.4230/LIPIcs.FSTTCS.2014.379

Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL:https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.FSTTCS.2014.379,doi:10.4230/LIPIcs.FSTTCS.2014.379. 5 E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy. In[1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pages 368–377, 1991.doi:10.1109/SFCS...

work page doi:10.4230/lipics.fsttcs.2014.379 2014
[5]

7 Eryk Kopczyński

URL:https://doi.org/10.1016/0168-0072(94)90086-8, doi: 10.1109/LICS.1992.185550. 7 Eryk Kopczyński. Half-positional determinacy of infinite games. In Michele Bugliesi, Bart Pren- eel, Vladimiro Sassone, and Ingo Wegener, editors,Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Pa...

work page doi:10.1016/0168-0072(94)90086-8 1992
[6]

Differential Privacy

doi:10.1007/11787006\_29. 8 Eryk Kopczyński. Omega-regular half-positional winning conditions. In Jacques Duparc and Thomas A. Henzinger, editors,Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 ofLecture Notes in Computer Science, pag...

work page doi:10.1007/11787006 2007
[7]

9 Pierre Ohlmann

doi:10.1007/978-3-540-74915-8\_7. 9 Pierre Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. TheoretiCS, Volume 2, jan

work page doi:10.1007/978-3-540-74915-8
[8]

URL: http://dx.doi.org/10.46298/theoretics.23.3, doi:10.46298/theoretics.23.3

work page doi:10.46298/theoretics.23.3