arXiv subjects

Thomas Colcombet

Publications and source records attributed to Thomas Colcombet.

At least 19 recordsLinked to original sources

arXiv2026

An algebraic characterisation of Eve-positional languages

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.

cs.FL↗

arXiv2026

Expregular functions

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\~{\^{e}}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 $\omega$-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.

cs.FL↗

arXiv2025

Regular expressions over countable words

We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular languages - defined over finite words and characterized by automata, monadic second-order logic, and regular expressions - to the setting of countable words. In this paper, we introduce and study five classes of expressions: marked star-free expressions, marked expressions, power-free expressions, scatter-free expressions, and scatter expressions. We show that these expression classes characterize natural fragments of logic over countable words and possess decidable algebraic characterizations. As part of our algebraic analysis, we provide a precise description of the relevant classes in terms of their J-class structure. These results complete a triad of equivalences - between logic, algebra, and expressions - in this richer setting, thereby generalizing foundational results from classical formal language theory.

cs.LO↗

arXiv2024

Tree algebras and bisimulation-invariant MSO on finite graphs

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognized by finitary tree algebras are the regular ones, ie. the ones expressible in mu-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.

cs.LO↗

arXiv2023

From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History) Determinism

We study transformations of automata and games using Muller conditions into equivalent ones using parity or Rabin conditions. We present two transformations, one that turns a deterministic Muller automaton into an equivalent deterministic parity automaton, and another that provides an equivalent history-deterministic Rabin automaton. We show a strong optimality result: the obtained automata are minimal amongst those that can be derived from the original automaton by duplication of states. We introduce the notions of locally bijective morphisms and history-deterministic mappings to formalise the correctness and optimality of these transformations. The proposed transformations are based on a novel structure, called the alternating cycle decomposition, inspired by and extending Zielonka trees. In addition to providing optimal transformations of automata, the alternating cycle decomposition offers fundamental information on their structure. We use this information to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions and to perform a systematic study of a normal form for parity automata.

cs.FL↗

arXiv2022

Playing Safe, Ten Years Later

We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety objectives. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety objective is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety objectives without any regularity assumptions. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.

cs.GT↗

arXiv2022

Z-polyregular functions

This paper introduces a robust class of functions from finite words to integers that we call Z-polyregular functions. We show that it admits natural characterizations in terms of logics, Z-rational expressions, Z-rational series and transducers. We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that first-order definability of Z-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity.

cs.FL↗

arXiv2022

On the size of good-for-games Rabin automata and its link with the memory in Muller games

In this paper, we look at good-for-games Rabin automata that recognise a Muller language (a language that is entirely characterised by the set of letters that appear infinitely often in each word). We establish that minimal such automata are exactly of the same size as the minimal memory required for winning Muller games that have this language as their winning condition. We show how to effectively construct such minimal automata. Finally, we establish that these automata can be exponentially more succinct than equivalent deterministic ones, thus proving as a consequence that chromatic memory for winning a Muller game can be exponentially larger than unconstrained memory.

cs.FL↗

arXiv2022

First-order separation over countable ordinals

We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on $\omega$-words. For this, we develop the algebraic concept of monoid (resp. $\omega$-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. $\omega$-semigroup, resp. ordinal monoid) that explicitly includes a new operation capturing the loss of precision induced by first-order indistinguishability. We also show the computability of FO-pointlike sets, and the decidability of the covering problem for first-order logic on countable ordinal words.

cs.LO↗

arXiv2021

The Theory of Universal Graphs for Infinite Duration Games

We introduce the notion of universal graphs as a tool for constructing algorithms solving games of infinite duration such as parity games and mean payoff games. In the first part we develop the theory of universal graphs, with two goals: showing an equivalence and normalisation result between different recently introduced related models, and constructing generic value iteration algorithms for any positionally determined objective. In the second part we give four applications: to parity games, to mean payoff games, to a disjunction between a parity and a mean payoff objective, and to disjunctions of several mean payoff objectives. For each of these four cases we construct algorithms achieving or improving over the best known time and space complexity.

cs.FL↗

arXiv2020

Optimal Transformations of Muller Conditions

In this paper, we are interested in automata over infinite words and infinite duration games, that we view as general transition systems. We study transformations of systems using a Muller condition into ones using a parity condition, extending Zielonka's construction. We introduce the alternating cycle decomposition transformation, and we prove a strong optimality result: for any given deterministic Muller automaton, the obtained parity automaton is minimal both in size and number of priorities among those automata admitting a morphism into the original Muller automaton. We give two applications. The first is an improvement in the process of determinisation of B\"uchi automata into parity automata by Piterman and Schewe. The second is to present characterisations on the possibility of relabelling automata with different acceptance conditions.

cs.FL↗

arXiv2020

Learning automata and transducers: a categorical approach

In this paper, we present a categorical approach to learning automata over words, in the sense of the $L^*$-algorithm of Angluin. This yields a new generic $L^*$-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a "computation category". We establish that the sufficient properties for yielding the existence of minimal automata (that were disclosed in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.

cs.FL↗

arXiv2020

Cost Automata, Safe Schemes, and Downward Closures

In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed $\lambda Y$-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power. The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties.

cs.FL↗

arXiv2019

Controlling a random population

Bertrand et al. introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min-cut theorem, and of the theory of regular cost functions. We introduce an intermediate problem of independence interest called the sequential flow problem and study its complexity.

cs.FL↗

arXiv2019

Unambiguous separators for tropical tree automata

In this paper we show that given a max-plus automaton (over trees, and with real weights) computing a function $f$ and a min-plus automaton (similar) computing a function $g$ such that $f\leqslant g$, there exists effectively an unambiguous tropical automaton computing $h$ such that $f\leqslant h\leqslant g$. This generalizes a result of Lombardy and Mairesse of 2006 stating that series which are both max-plus and min-plus rational are unambiguous. This generalization goes in two directions: trees are considered instead of words, and separation is established instead of characterization (separation implies characterization). The techniques in the two proofs are very different.

cs.FL↗

arXiv2019

On Reachability Problems for Low-Dimensional Matrix Semigroups

We consider the Membership and the Half-Space Reachability problems for matrices in dimensions two and three. Our first main result is that the Membership Problem is decidable for finitely generated sub-semigroups of the Heisenberg group over rational numbers. Furthermore, we prove two decidability results for the Half-Space Reachability Problem. Namely, we show that this problem is decidable for sub-semigroups of $\mathrm{GL}(2,\mathbb{Z})$ and of the Heisenberg group over rational numbers.

cs.CC↗

arXiv2018

Parity games and universal graphs

This paper is a contribution to the study of parity games and the recent constructions of three quasipolynomial time algorithms for solving them. We revisit a result of Czerwi\'nski, Daviaud, Fijalkow, Jurdzi\'nski, Lazi\'c, and Parys witnessing a quasipolynomial barrier for all three quasipolynomial time algorithms. The argument is that all three algorithms can be understood as constructing a so-called separating automaton, and to give a quasipolynomial lower bond on the size of separating automata. We give an alternative proof of this result. The key innovations of this paper are the notion of universal graphs and the idea of saturation.

cs.GT↗

arXiv2017

Automata Minimization: a Functorial Approach

In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as functors from input categories that specify the type of the languages and of the machines to categories that specify the type of outputs. Our results are as follows: A) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. B) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. C) We show how this framework can be instantiated to unify several phenomena in automata theory, starting with determinization, minimization and syntactic algebras. We provide explanations of Choffrut's minimization algorithm for subsequential transducers and of Brzozowski's minimization algorithm in this setting.

cs.LO↗