An algebraic characterisation of Eve-positional languages

AIPR assessment

This is a hard, active, and fairly specialized theory problem, not a crowded empirical benchmark. The main strengths reinforce one another: a clean semantic characterization, a simple local form, and a complete proof that connects directly to recent game-theoretic results. The main weaknesses also interact: there is no algorithmic consequence, no complexity analysis for checking the local properties, and the practical path from theorem to tool is indirect. The result is strongest as a reusable s

Abstract

We present a new algebraic characterisation of Eve-positionality for $ω$-regular languages. It involves only a limited number of elementary local properties to be checked. An $ω$-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 $ω$-regular languages. More precisely, it relies on their a 1-to-2 player lift result: for an $ω$-regular language, being Eve-positionally over all finite Eve-only arenas suffices for being Eve-positional over all two-player arenas.

Score Breakdown

More from this week

• Agentic World Modeling: Foundations, Capabilities, Laws, and Beyond
• How Hard is it to Decide if a Fact is Relevant to a Query?
• Railway Artificial Intelligence Learning Benchmark (RAIL-BENCH): A Benchmark Suite for Perception in the Railway Domain
• On first-order model checking parameterized by the number of variables
• Entrywise Low-Rank Approximation and Matrix \(p \rightarrow q\) Norms via Global Correlation Rounding

More in Logic

• Univalence without function extensionality
• Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
• An Undecidability Proof for the Plan Existence Problem
• On first-order model checking parameterized by the number of variables