Pierre Ohlmann

Antonio Casares, Pierre Ohlmann

In the context of 2-player zero-sum infinite-duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with <= k states of memory. For omega-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Sigma0^2), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory <= k, leading to the following results: (1) For omega-regular objectives, the memory over finite and infinite games coincides and can be computed in NP. (2) Given two objectives W1 and W2 in BC(Sigma0^2) and assuming W1 is prefix-independent, the memory of W1 U W2 is at most the product of the memories of W1 and W2. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.

Thomas Colcombet, Nathan Lhote, Pierre Ohlmann

Polyregular functions form a robust class of string-to-string functions with polynomial growth, as evidenced by Bojanczyk (2018). This class admits numerous descriptions and enjoys several closure properties. Most notably, polyregular functions are regularity reflecting (\ie the inverse image of a regular language is regular). In this work, we propose a robust class of string-to-string functions with exponential growth which we call expregular functions. We consider the following three models for describing them: - MSO set interpretations, which extend MSO interpretations (one of the models capturing polyregular functions), by operating on monadic variables instead of tuples of first-order variables; - yield-Hennie machines, which are branching one-tape Turing machines with bounded visit; and - Ariadne transducers, a new model of 2-way pushdown machines with a bounded visit restriction. Our main contribution is a translation from MSO set interpretations to yield-Hennie machines, which are known to be regularity reflecting (Dartois, Nguy\~{ê}n, Peyrat 2026). In particular this establishes that MSO set interpretations are regularity reflecting, which in turn settles a major conjecture about automatic structures: every automatic $ω$-word has a decidable MSO theory. Yield-Hennie machine directly translate to Ariadne transducers, and our second contribution is to prove that Ariadne transducers also translate to MSO set interpretations, thus establishing the equivalence of the three models. This is obtained by showing that Ariadne automata -- the automaton model corresponding to Ariadne transducers -- recognise regular languages.

Mikołaj Bojańczyk, Pierre Ohlmann

The Pathwidth Theorem states that if a class of graphs has unbounded pathwidth, then it contains all trees as graph minors. We prove a similar result for dense graphs. More precisely, we give a finite family of tree-like patterns and prove that every graph class of bounded cliquewidth and unbounded linear cliquewidth contains arbitrarily large patterns as induced subgraphs. These patterns mso transduce all trees, and fo transduce subdivisions of all binary trees. In particular, our result provides the missing piece in establishing that the cmso transduction order is total over classes of finite graphs.

Antonio Casares, Pierre Ohlmann, Michał Skrzypczak et al.

This paper contributes to the study of positional determinacy of infinite duration games played on potentially infinite graphs with neutral transitions. Recently, [Ohlmann, TheoretiCS 2023] established that positionality of prefix-independent objectives is preserved by finite lexicographic products. We propose two different notions of infinite lexicographic products indexed by arbitrary ordinals, and extend Ohlmann's result by proving that they also preserve positionality. In the context of one-player positionality, this extends positional determinacy results of [Grädel and Walukiewicz, Logical Methods in Computer Science 2006] to edge-labelled games and arbitrarily many priorities for both Max-Parity and Min-Parity. Moreover, we show that the Max-Parity objectives over countable ordinals are complete for the infinite levels of the difference hierarchy over $Σ^0_2$ and that Min-Parity is complete for the class $Σ^0_3$. We obtain therefore positional languages that are complete for all those levels, as well as new insights about closure under unions and neutral letters.

Pierre Ohlmann, Michał Skrzypczak

We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in Σ_0^2 which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective W which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective W' which is equivalent to W over finite game graphs and positional over arbitrary game graphs.

Pierre Ohlmann

We propose a new deterministic symmetric recursive algorithm for solving mean-payoff games.

Nathanaël Fijalkow, Guillaume Lagarde, Théo Matricon et al.

We consider the problem of automatically constructing computer programs from input-output examples. We investigate how to augment probabilistic and neural program synthesis methods with new search algorithms, proposing a framework called distribution-based search. Within this framework, we introduce two new search algorithms: Heap Search, an enumerative method, and SQRT Sampling, a probabilistic method. We prove certain optimality guarantees for both methods, show how they integrate with probabilistic and neural techniques, and demonstrate how they can operate at scale across parallel compute environments. Collectively these findings offer theoretical and applied studies of search algorithms for program synthesis that integrate with recent developments in machine-learned program synthesizers.