An algebraic characterisation of Eve-positional languages

TL;DR

This paper introduces a new algebraic framework to characterize Eve-positionality in omega-regular languages, simplifying the verification process by using elementary local properties.

Contribution

It provides an algebraic characterization of Eve-positionality that relies on a limited set of local properties, building on recent theoretical results.

Findings

Eve-positionality can be characterized algebraically.

The new characterization simplifies checking Eve-positionality.

Relies on recent lift results connecting finite and two-player arenas.

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.