Publications of Thomas Colcombet
You can also find my publications on DBLP, on HAL or on arXiv (for some of
them).
But think:
Do you really need to take the plane for populating your publication
list?
I have been travelling a lot for conferences. These were times of glory, but reckless
times. Some reflections about this subject in this blog post.
2025
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 recognised by finitary tree
algebras whose sorts zero and one are finite 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.
Thomas Colcombet and
Alexander Rabinovich. “
On the Expansion of Monadic
Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates”. 33rd
EACSL Annual Conference on Computer Science Logic, CSL 2025, February 10-14,
2025, Amsterdam, Netherlands, 2025, pages 11:1–11:26. LIPIcs, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Jörg Endrullis and
Sylvain Schmitz. Doi
10.4230/LIPICS.CSL.2025.11.
In this work, we consider two
extensions of monadic second-order logic, and study in what cases the classical
decidability results are preserved.
The first extension, MSO[CBrank],
is MSO (over the signature of the binary tree) augmented with the extra
ability to express that the subtree over a set X has Cantor-Bendixson rank
, for some fixed
countable ordinal .
We show that this extension is decidable over the binary tree if and only if
is
finite, which means that it is decidable if and only if it is equivalent in expressiveness
to MSO.
The second extension, MSO[otp],
is MSO (over the signature of order) augmented with the extra ability
to express that the suborder induced by a set X has order type
for some fixed
countable ordinal .
We show that this extension is decidable over countable ordinals if and only if
,
which means that it is decidable if and only if it is equivalent in expressiveness to
MSO.
The first result can be established as a consequence of the second.
The second result relies on the undecidability results of the logic
BMSO (itself relying on the undecidability of MSO+U) in the case of
for
a limit ordinal, and on entirely new techniques when
is a
successor ordinal. We also have some partial extensions of the second result to some
uncountable cases.
2024
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.
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.
2023
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.
Thomas Colcombet,
Gaëtan Douéneau-Tabot, and
Aliaume Lopez.
“
-polyregular
functions”. LICS, 2023, pages 1–13. Doi
10.1109/LICS56636.2023.10175685.
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.
2022
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.
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
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.
Thomas Colcombet,
Sam van Gool, and
Rémi Morvan. “
First-order separation
over countable ordinals”. Foundations of Software Science and Computation
Structures - 25th International Conference, FOSSACS 2022, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS
2022, Munich, Germany, April 2-7, 2022, Proceedings, 2022, pages 264–284.
Lecture Notes in Computer Science, Springer. Editors
Patricia Bouyer and
Lutz Schröder. Doi
10.1007/978-3-030-99253-8_14.
We show
that the existence of a first-order formula separa- ting 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
-words.
For this, we develop the algebraic concept of monoid (resp.
-semigroup,
resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp.
-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.
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.
Thomas Colcombet and
Arthur Jaquard. “
A Complexity Approach to Tree
Algebras: the Polynomial Case”. 47th International Symposium on Mathematical
Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna,
Austria, 2022, pages 37:1–37:14. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. Editors
Stefan Szeider,
Robert Ganian, and
Alexandra Silva.
Doi
10.4230/LIPIcs.MFCS.2022.37.
In this paper, we consider
infinitely sorted tree algebras recognising regular language of finite trees. We
pursue their analysis under the angle of their asymptotic complexity, i.e.
the asymptotic size of the sorts as a function of the number of variables
involved.
Our main result establishes an equivalence between the languages recognised by
algebras of polynomial complexity and the languages that can be described by
nominal word automata that parse linearisation of the trees. On the way, we show
that for such algebras, having polynomial complexity corresponds to having
uniformly boundedly many orbits under permutation of the variables, or
having a notion of bounded support (in a sense similar to the one in nominal
sets).
We also show that being recognisable by an algebra of polynomial complexity is a
decidable property for a regular language of trees.
Given an MSO formula
with free variables
, one can define
the function
mapping a word w to the number of valuations satisfying
in
. In
this paper, we introduce the class of Z-linear combinations of such functions, that we
call Z-polyregular functions. Indeed, it turns out to be closely related to the
well-studied class of polyregular functions.
The main result of this paper solve two natural decision problems for
Z-polyregular functions. First, we show that one can minimise the number
of
free variables which are needed to describe a function. Then, we show how to decide
if a function can be defined using first-order formulas, by extending the notion
of residual automaton and providing an original semantic characterisation
based on aperiodicity. We also connect this class of functions to Z-rational
series.
Antonio Casares,
Thomas Colcombet, and
Karoliina Lehtinen. “
On the Size of
Good-For-Games Rabin Automata and Its Link with the Memory in Muller
Games”. ICALP 2022, 2022, pages 117:1–117:20. LIPIcs, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Mikołaj Bojańczyk, Emanuela Merelli,
and
David P. Woodruff. Doi
10.4230/LIPIcs.ICALP.2022.117.
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.
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
-words.
For this, we develop the algebraic concept of monoid (resp.
-semigroup,
resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp.
-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.
2021
Thomas Colcombet and
Arthur Jaquard. “
A Complexity Approach to Tree
Algebras: the Bounded Case”. 48th International Colloquium on Automata,
Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland
(Virtual Conference), 2021, pages 127:1–127:13. LIPIcs, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Nikhil Bansal, Emanuela Merelli,
and
James Worrell. Doi
10.4230/LIPIcs.ICALP.2021.127.
In this
paper, we initiate a study of the expressive power of tree algebras, and more
generally infinitely sorted algebras, based on their asymptotic complexity. We
provide a characterization of the expressiveness of tree algebras of bounded
complexity.
Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as
well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set
indexed by a parameter that can be interpreted as the number of variables or hole
types. Finite such algebras—meaning when all sorts are finite—can be classified
depending on the asymptotic size of the carrier sets as a function of the parameter,
that we call the complexity of the algebra. This naturally defines the notions of
algebras of bounded, linear, polynomial, exponential or doubly exponential
complexity...
We initiate in this work a program of analysis of the complexity of infinitely
sorted algebras. Our main result precisely characterizes the tree algebras of
bounded complexity based on the languages that they recognize as Boolean
closures of simple languages. Along the way, we prove that such algebras that
are syntactic (minimal for a language) are exactly those in which, as soon
as there are sufficiently many variables, the elements are invariant under
permutation of the variables. Tree algebras in many of their forms, such
as clones, hyperclones, operads, etc, as well as other kind of algebras, are
infinitely sorted: the carrier is a multi sorted set indexed by a parameter that
can be interpreted as the number of variables or hole types. Finite such
algebras—meaning when all sorts are finite—can be classified depending on
the asymptotic size of the carrier sets as a function of the parameter, that
we call the complexity of the algebra. This naturally defines the notions of
algebras of bounded, linear, polynomial, exponential or doubly exponential
complexity...
We initiate in this work a program of analysis of the complexity of infinitely
sorted algebras. Our main result precisely characterizes the tree algebras of bounded
complexity based on the languages that they recognize as Boolean closures of simple
languages. Along the way, we prove that such algebras that are syntactic (minimal
for a language) are exactly those in which, as soon as there are sufficiently many
variables, the elements are invariant under permutation of the variables.
Antonio Casares,
Thomas Colcombet, and
Nathanaël Fijalkow. “
Optimal
Transformations of Games and Automata Using Muller Conditions”. 48th
International Colloquium on Automata, Languages, and Programming, ICALP 2021,
July 12-16, 2021, Glasgow, Scotland (Virtual Conference), 2021, pages 123:1–123:14.
LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Editors
Nikhil Bansal,
Emanuela Merelli, and
James Worrell. Doi
10.4230/LIPIcs.ICALP.2021.123.
We consider the following question: given an automaton or a game with a
Muller condition, how can we efficiently construct an equivalent one with a parity
condition? There are several examples of such transformations in the literature,
including in the determinisation of Büchi automata.
We define a new transformation called the alternating cycle decomposition,
inspired and extending Zielonka’s construction. Our transformation operates on
transition systems, encompassing both automata and games, and preserves semantic
properties through the existence of a locally bijective morphism. We show a strong
optimality result: the obtained parity transition system is minimal both in
number of states and number of priorities with respect to locally bijective
morphisms.
We give two applications: the first is related to the determinisation of
Büchi automata, and the second is to give crisp characterisations on the
possibility of relabelling automata with different acceptance conditions.
Thomas Colcombet. “
The factorisation forest theorem”. Handbook of Automata
Theory, 2021, pages 653–693. European Mathematical Society Publishing House,
Zürich, Switzerland. Editor
Jean-Éric Pin. Doi
10.4171/Automata-1/18.
A chapter describing Simon’s theorem on factorisation forest, and some recent
developments.
The factorisation forest theorem describes Ramsey-like decomposition of words in
a semigroup.
The chapter describes various equivalent statement of the theorem, in particular
using the notion of split. Some applications are described, in particular in the
theory of semigroups and for matrices in the tropical semiring. Extensions to
infinite linear orders, as well as deterministic variants are also covered.
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.
Thomas Colcombet,
Daniela Petrişan, and
Riccardo Stabile. “
Learning
Automata and Transducers: A Categorical Approach”. 29th EACSL Annual
Conference on Computer Science Logic, CSL 2021, January 25-28, 2021,
Ljubljana, Slovenia (Virtual Conference), 2021, pages 15:1–15:17. LIPIcs, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. Editors
Christel Baier and Jean
Goubault-Larrecq. Doi
10.4230/LIPIcs.CSL.2021.15.
In this paper, we
present a categorical approach to learning automata over words, in the sense of the
-algorithm of Angluin. This
yields a new generic -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.
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, and to combinations of them (in the form of
disjunctions of objectives). For each of these four cases we construct algorithms
achieving or improving over the best known time and space complexity.
2020
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.
David Barozzini,
Lorenzo Clemente,
Thomas Colcombet, and
Paweł
Parys. “
Cost Automata, Safe Schemes, and Downward Closures”. 47th
International Colloquium on Automata, Languages, and Programming, ICALP
2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), 2020,
pages 109:1–109:18. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. Editors Artur Czumaj,
Anuj Dawar, and Emanuela Merelli. Doi
10.4230/LIPIcs.ICALP.2020.109.
Higher-order recursion schemes are an
expressive formalism used to define languages of possibly infinite ranked trees. They
extend regular and context-free grammars, and are equivalent to simply typed
-calculus
and collapsible pushdown automata. In this work we prove, under a syntactical
constraint called safety, decidability of the model-checking problem for recursion
schemes against properties defined by alternating B-automata, an extension of
alternating parity automata for infinite trees with a boundedness acceptance
condition. We then exploit this result to show how to compute downward
closures of languages of finite trees recognized by safe recursion schemes.
In this paper, we present a
categorical approach to learning automata over words, in the sense of the
-algorithm of Angluin. This
yields a new generic -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.
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üchi automata into parity automata by
Piterman and Schewe. The second is to present characterisations on the
possibility of relabelling automata with different acceptance conditions.
Higher-order recursion schemes are an expressive
formalism used to define languages of possibly infinite ranked trees. They
extend regular and context-free grammars, and are equivalent to simply typed
-calculus
and collapsible pushdown automata. In this work we prove, under a syntactical
constraint called safety, decidability of the model-checking problem for recursion
schemes against properties defined by alternating B-automata, an extension of
alternating parity automata for infinite trees with a boundedness acceptance
condition. We then exploit this result to show how to compute downward
closures of languages of finite trees recognized by safe recursion schemes.
Thomas Colcombet and
Sylvain Lombardy. “
Unambiguous Separators for
Tropical Tree Automata”. 37th International Symposium on Theoretical Aspects of
Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France, 2020,
pages 32:1–32:13. Doi
10.4230/LIPIcs.STACS.2020.32.
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
, there
exists effectively an unambiguous tropical automaton computing h such that
.
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.
Thomas Colcombet,
Nathanaël Fijalkow, and
Pierre Ohlmann. “
Controlling a
Random Population”. Foundations of Software Science and Computation Structures -
23rd International Conference, FOSSACS 2020, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2020, Dublin,
Ireland, April 25-30, 2020, Proceedings, 2020, pages 119–135. Editors Jean
Goubault-Larrecq and Barbara König. Doi
10.1007/978-3-030-45231-5_7.
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.
2019
Thomas Colcombet,
Joël Ouaknine,
Pavel Semukhin, and
James Worrell. “
On
Reachability Problems for Low-Dimensional Matrix Semigroups”. 46th International
Colloquium on Automata, Languages, and Programming (ICALP 2019),
2019, pages 44:1–44:15. Leibniz International Proceedings in Informatics
(LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. Editors
Christel
Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi. Doi
10.4230/LIPIcs.ICALP.2019.44.
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 GL(2,Z) and of the Heisenberg group over rational numbers.
Thomas Colcombet and
Nathanaël Fijalkow. “
Universal Graphs and Good for
Games Automata: New Tools for Infinite Duration Games”. Foundations of Software
Science and Computation Structures, FOSSACS 2019, 2019, pages 1–26. Springer.
Editors
Mikołaj Bojańczyk and Alex Simpson. Doi
10.1007/978-3-030-17127-8_1.
In this paper, we give a self contained presentation of a recent
breakthrough in the theory of infinite duration games: the existence of a
quasipolynomial time algorithm for solving parity games. We introduce for this
purpose two new notions: good for small games automata and universal
graphs.
The first object, good for small games automata, induces a generic algorithm for
solving games by reduction to safety games. We show that it is in a strong sense
equivalent to the second object, universal graphs, which is a combinatorial notion
easier to reason with. Our equivalence result is very generic in that it holds for all
existential memoryless winning conditions, not only for parity conditions.
2018
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ński,
Daviaud, Fijalkow, Jurdziński, Lazić, 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.
Olivier Carton,
Thomas Colcombet, and
Gabriele Puppis. “
An algebraic
approach to MSO-definability on countable linear orderings”. The Journal of
Symbolic Logic, 2018, pages 1147–1189. Cambridge University Press. Doi
10.1017/jsl.2018.7.
We develop an algebraic notion of recognizability for
languages of words indexed by countable linear orderings. We prove that
this notion is effectively equivalent to definability in monadic second-order
(MSO) logic. We also provide three logical applications. First, we establish
the first known collapse result for the quantifier alternation of MSO logic
over countable linear orderings. Second, we solve an open problem posed
by Gurevich and Rabinovich, concerning the MSO-definability of sets of
rational numbers using the reals in the background. Third, we establish the
MSO-definability of the set of yields induced by an MSO-definable set of trees,
confirming a conjecture posed by Bruyère, Carton, and Sénizergues.
2017
We show how recent results concerning quantitative forms of
automata help providing refined understanding of the properties of a system (for
instance, a program). In particular, combining the size-change abstraction
together with results concerning the asymptotic behavior of tropical au-
tomata yields extremely fine complexity analysis of some pieces of code.
Thomas Colcombet. “
Logic and Regular Cost Functions”. LICS, 2017, pages 1–4.
IEEE Computer Society. Note: Invited tutorial. Doi
10.1109/LICS.2017.8005061.
Regular cost functions offer a toolbox for automatically solving
problems of existence of bounds, in a way similar to the theory of regular languages.
More precisely, it allows to test the existence of bounds for quantities that can be
defined in cost monadic second-order logic (a quantitative variant of monadic
second-order logic) with inputs that range over finite words, infinite words, finite
trees, and (sometimes) infinite trees.
Though the initial results date from the works of Hashiguchi in the early eighties,
it is during the last decade that the theory took its current shape and that many new
results and applications have been established.
In this tutorial, two connections linking logic with the theory of regular cost
functions will be described. The first connection is a proof of a result of
Blumensath, Otto and Weyer stating that it is decidable whether the fixpoint of
a monadic second- order formula is reached within a bounded number of
iterations over the class of infinite trees. The second connection is how non-
standard models (and more precisely non-standard analysis) give rise to a
unification of the theory of regular cost functions with the one of regular
languages.
In this paper we regard languages and their acceptors – such as
deterministic or weighted automata or transducers – 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 and
minimization (which have been previously studied from a coalgebraic and duality
theoretic perspective). We also show how subsequential transducers can be seen as
functors valued in a Kleisli category and explain Choffrut’s minimization algorithm.
We also give an alternative proof of correctness of Brzozowski’s minimization
algorithm.
Already in the seventies, strong results illustrating the intimate relationship
between category theory and automata theory have been described and are
still investigated. In this column, we provide a uniform presentation of the
basic concepts that underlie minimization results in automata theory. We
then use this knowledge for introducing a new model of automata that is
an hybrid of deterministic finite automata and automata weighted over a
field. These automata are very natural, and enjoy minimization result by
design.
The presentation of this paper is indeed categorical in essence, but it assumes no
prior knowledge from the reader. It is also non-conventional in that it is neither
algebraic, nor co-algebraic oriented.
Thomas Colcombet and
Daniela Petrişan. “
Automata in the Category of Glued
vector spaces”. MFCS 2017: Mathematical Foundations of Computer Science, 2017,
pages 52:1–52:14. Doi
10.4230/LIPIcs.MFCS.2017.52.
In this paper,
we adopt of categorical approach to the conception of automata classes enjoying
minimisation by design. The main instantiation of this construction is the new class
of automata that are hybrid between deterministic and vector space automata.
We introduce perfect half space games, in
which the goal of Player 2 is to make the sums of encountered multi-dimensional
weights diverge in a direction which is consistent with a chosen sequence
of perfect half spaces (chosen dynamically by Player 2). We establish that
the bounding games of Jurdzinski et al. (ICALP 2015) can be reduced to
perfect half space games, which in turn can be translated to the lexicographic
energy games of Colcombet and Niwinski, and are positionally determined
in a strong sense (Player 2 can play without knowing the current perfect
half space). We finally show how perfect half space games and bounding
games can be employed to solve multi-dimensional energy parity games in
pseudo-polynomial time when both the numbers of energy dimensions and of
priorities are fixed, regardless of whether the initial credit is given as part of the
input or existentially quantified. This also yields an optimal 2-EXPTIME complexity
with given initial credit, where the best known upper bound was non-elementary.
We define a new class of
languages of -words,
strictly extending -regular
languages. One way to present this new class is by a type of
regular expressions. The new expressions are an extension of
-regular
expressions where two new variants of the Kleene star
are
added:
and .
These new exponents are used to say that parts of the input word have bounded size,
and that parts of the input can have arbitrarily large sizes, respectively. For instance, the
expression
represents the language of infinite words over the letters
where there is a common bound on the number of consecutive letters
. The
expression
represents a similar language, but this time the distance between consecutive
’s is
required to tend toward the infinite. We develop a theory for these languages, with a
focus on decidability and closure. We define an equivalent automaton model,
extending Büchi automata. The main technical result is a complementation
lemma that works for languages where only one type of exponent—either
or
—is
used. We use the closure and decidability results to obtain partial decidability results
for the logic MSOLB, a logic obtained by extending monadic second-order logic with
new quantifiers that speak about the size of sets.
2016
Thomas Colcombet and
Nathanaël Fijalkow. “
The Bridge Between Regular
Cost Functions and Omega-Regular Languages”. 43rd International Colloquium on
Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016,
Rome, Italy, 2016, pages 126:1–126:13. Doi
10.4230/LIPIcs.ICALP.2016.126.
In this paper, we exhibit a one-to-one correspondence between
-regular
languages and a subclass of regular cost functions over finite words, called
-regular
like cost functions. This bridge between the two models allows one to readily import
classical results such as the last appearance record or the McNaughton-Safra
constructions to the realm of regular cost functions. In combination with game
theoretic techniques, this also yields an optimal and simple procedure of
history-determinisation for cost automata, a central result in the theory of regular
cost functions.
Thomas Colcombet and
Laure Daviaud. “
Approximate Comparison of Functions
Computed by Distance Automata”. Theory Comput. Syst., 2016, pages 579–613. Doi
10.1007/s00224-015-9643-3.
Distance automata are automata weighted over the
semiring
(the tropical semiring). Such automata compute functions from words to
.
It is known from Krob that the problems of deciding
‘
’ or
‘
’ for
and
computed by distance automata is an undecidable problem. The main contribution of
this paper is to show that an approximation of this problem is decidable.
We present an algorithm which, given
and two
functions
computed by distance automata, answers “yes” if
, “no”
if ,
and may answer “yes” or “no” in all other cases. This result highly refines previously
known decidability results of the same type.
The core argument behind this quasi-decision procedure is an algorithm which is
able to provide an approximated finite presentation of the closure under products of
sets of matrices over the tropical semiring.
We also establish another theorem, of affine domination, stating that previously
known decision procedures for cost-automata have an improved precision when used
over distance automata.
Thomas Colcombet and
Stefan Göller. “
Games with bound guess actions”.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS ’16, New York, NY, USA, July 5-8, 2016, 2016, pages 257–266. Doi
10.1145/2933575.2934502.
We introduce games with (bound) guess
actions. These are games in which the players may be asked along the play to
provide numbers that need to satisfy some bounding constraints. These
are natural extensions of domination games occurring in the regular cost
function theory. In this paper we consider more specifically the case where the
constraints to be bounded are regular cost functions, and the long term goal is an
-regular
winning condition. We show that such games are decidable on finite arenas.
Regular
cost functions form a quantitative extension of regular languages that share
the array of characterisations the latter possess. In this theory, functions
are treated only up to preservation of boundedness on all subsets of the
domain. In this work, we subject the well known distance automata (also called
min-automata), and their dual max-automata to this framework, and obtain a
number of effective characterisations in terms of logic, expressions and algebra.
Achim Blumensath,
Thomas Colcombet, and
Paweł Parys. “
On a Fragment
of AMSO and Tiling Systems”. 33rd Symposium on Theoretical Aspects
of Computer Science (STACS 2016), 2016, pages 19:1–19:14. Leibniz
International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Nicolas Ollinger and
Heribert Vollmer. Doi
http://dx.doi.org/10.4230/LIPIcs.STACS.2016.19.
We prove that
satisfiability over infinite words is decidable for a fragment of asymptotic
monadic second-order logic. In this fragment we only allow formulae of the form
,
where
does not use quantifiers over number variables, and variables r and
s can be only used simul- taneously, in subformulae of the form
.
2015
The notion of orbit finite data monoid was
recently introduced by Bojanczyk as an algebraic object for defining recognizable
languages of data words. Following Buchi’s approach, we introduce a variant of
monadic second-order logic with data equality tests that captures precisely the data
languages recognizable by orbit finite data monoids. We also establish, following this
time the approach of Schutzenberger, McNaughton and Papert, that the first-order
fragment of this logic defines exactly the data languages recognizable by aperiodic
orbit finite data monoids. Finally, we consider another variant of the logic that can
be interpreted over generic structures with data. The data languages defined in
this variant are also recognized by unambiguous finite memory automata.
Thomas Colcombet. “
Non-ambiguity in Automata Theory”. Descriptional
Complexity of Formal Systems - 17th International Workshop, DCFS 2015, 2015,
pages 3–18. Lecture Notes in Computer Science, Springer. Editors
Jeffrey
Shallit and
Alexander Okhotin. Doi
10.1007/978-3-319-19225-3˙1.
Determinism of devices is a key aspect throughout all of computer science, simply
for considerations of efficiency of the implementation. One possible way
(among others) to relax this notion is to consider unambiguous machines:
nondeterministic machines that have at most one accepting input on each
entry.
In this talk, we will investigate the nature of non-ambiguity in automata theory,
surveying the cases of standard finite words up to infinite trees, as well as
data-words. The goal of this talk will be to show how this notion of unambiguity is so
far not well understood, yielding to difficult open questions. In the last part, I will
present recent results with Gabriele Puppis and Michal Skrypczak that provide a
deep insight in the data-word case.
In this
paper, we study several sublogics of monadic second-order logic over countable linear
orderings, such as first-order logic, first-order logic on cuts, weak monadic
second-order logic, weak monadic second-ordered logic with cuts, as well as
fragments of monadic second-order logic in which sets have to be well ordered or
scattered.
We give decidable algebraic characterizations of all these logics and compare their
respective expressive power.
Given a formula phi(x,X) positive
in X , the boundedness problem asks whether the fixpoint induced by phi is reached
within some uniform bound independent of the structure (i.e. whether the fixpoint is
spurious, and can in fact be captured by a finite unfolding of the formula). In this
paper, we study the boundedness problem when phi is in the guarded fragment or
guarded negation fragment of first-order logic, or the fixpoint extensions of these
logics. It is known that guarded logics have many desirable computational and model
theoretic properties, including in some cases decidable boundedness. We
prove that boundedness for guarded negation fixpoint logic is decidable,
and even 2EXPTIME-complete. Our proof extends the connection between
guarded logics and automata, reducing boundedness for guarded logics to a
question about cost automata on trees, a type of automaton with counters
that assigns a natural number to each input rather than just a boolean.
Thomas Colcombet and
Amaldev Manuel. “
Combinatorial Expressions and
Lowerbounds”. 32nd International Symposium on Theoretical Aspects of
Computer Science, STACS 2015, 2015, pages 249–261. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Ernst W. Mayr and
Nicolas Ollinger. Doi
10.4230/LIPIcs.STACS.2015.249.
A new paradigm, called
combinatorial expressions, for computing functions expressing properties over an
infinite domains is introduced. The main result is a generic technique, for showing
indefinability of certain functions by the expressions, which uses a result, namely
Hales-Jewett theorem, from Ramsey theory. An application of the technique for
proving inexpressibility results for logics on metafinite structures is given. Apart
from this, some extensions and normal form theorems are also presented.
Thomas Colcombet and
Amaldev Manuel. “
Fragments of Fixpoint Logic on Data
Words”. 35th IARCS Annual Conference on Foundation of Software Technology and
Theoretical Computer Science, FSTTCS 2015, 2015, pages 98–111. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. Editors
Prahladh Harsha and
G. Ramalingam.
Doi
10.4230/LIPIcs.FSTTCS.2015.98.
We study two fragments of a
fixpoint logic on data words that enjoy Boolean closure, and contain previously
defined logics, namely two-variable first order logic and DataLTL. Our main
contribution is the separation of these two classes using a reduction to circuit
inexpressibility.
2014
The notion of orbit
finite data monoid was recently introduced by Bojańczyk as an algebraic
object for defining recognizable languages of data words. Following Buuchi’s
approach, we introduce a variant of monadic second-order logic with data
equality tests that captures precisely the data languages recognizable by orbit
finite data monoids. We also establish, following this time the approach of
Schutzenberger, McNaughton and Papert, that the first-order fragment of
this logic defines exactly the data languages recognizable by aperiodic orbit
finite data monoids. Finally, we consider another variant of the logic that
can be interpreted over generic structures with data. The data languages
defined in this variant are also recognized by unambiguous finite memory
automata.
Thomas Colcombet and
Amaldev Manuel. “
Generalized Data Automata and
Fixpoint Logic”. FSTTCS 2014: Foundations of Software Technology and Theoretical
Computer Science, 2014, pages 267–278. LIPICs, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. Editors
Venkatesh Raman and
S. P. Suresh.
Data
-words are
-words
where each position is additionally labelled by a data value from an infinite
alphabet. They can be seen as graphs equipped with two sorts of edges:
‘next position’ and ‘next position with the same data value’. Based on this
view, an extension of Data Automata called Generalized Data Automata
(GDA) is introduced. While the decidability of emptiness of GDA is open, the
decidability for a subclass class called Büchi GDA is shown using Multicounter
Automata. Next a natural fixpoint logic is defined on the graphs of data
-words and it is shown
that the -fragment
as well as the alternation-free fragment is undecidable. But the fragment which is
defined by limiting the number of alternations between future and past formulas is
shown to be decidable, by first converting the formulas to equivalent alternating
Büchi automata and then to Büchi GDA.
We consider
two-player games over graphs and give tight bounds on the memory size of
strategies ensuring safety conditions. More specifically, we show that the
minimal number of memory states of a strategy ensuring a safety condition is
given by the size of the maximal antichain of left quotients with respect
to language inclusion. This result holds for all safety conditions without
any regularity assumptions, and for all (finite or infinite) graphs of finite
degree.
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 optimal positional strategies in
games with counters.
Max-plus automata
(over
)
are finite devices that map input words to non-negative integers or
. In
this paper we present (a) an algorithm allowing to compute the asymptotic behaviour
of max-plus automata, and (b) an application of this technique to the evaluation of
the computational time complexity of programs.
(a) Given a max-plus automaton computing a function
, we show that the longest
word of value at most
for has
length ,
where
is a computable rational number (or is infinite).
(b) The size-change abstraction (SCA) is an a computational model used for
abstracting the behaviour of real programs.
Thanks to result (a), we show that the computational time
complexity of terminating SCA instances is decidable: the maximal
length of any sequence of transitions is exactly of asymptotic order
, where
is a computable rational
number and where
is the maximal value of the variables in the program.
Regular cost functions provide a
quantitative extension of regular languages that retains most of their important
properties, such as expressive power and decidability, at least over finite
and infinite words and over finite trees. Much less is known over infinite
trees.
We consider cost functions over infinite trees defined by an extension of weak
monadic second-order logic with a new fixed- point-like operator. We show this logic
to be decidable, improving previously known decidability results for cost logics over
infinite trees. The proof relies on an equivalence with a form of automata with
counters called quasi-weak cost automata, as well as results about converting
two-way alternating cost automata to one-way alternating cost automata.
In this paper we introduce so-called asymptotic logics, logics
that are meant to reason about weights of elements in a model in a way
inspired by topology. Our main subject of study is Asymptotic Monadic
Second-Order Logic over infinite words. This is a logic talking about
-words
labelled by integers. It contains full monadic second-order logic and can express
asymptotic properties of integers labellings.
We also introduce several variants of this logic and investigate their relationship
to the logic MSO+U. In particular, we compare their expressive powers by studying
the topological complexity of the different models. Finally, we introduce a certain
kind of tiling problems that is equivalent to the satisfiability problem of the weak
fragment of asymp- totic monadic second-order logic, i.e., the restriction with
quantification over finite sets only.
2013
Thomas Colcombet. “
The Factorisation Forest Theorem”. 2013. Note: To appear
in the handbook “Automata: from Mathematics to Applications”. 37 pages..
This chapter is devoted to the presentation of the factorisation forest theorem, a deep
result due to Simon, which provides advanced Ramsey-like arguments in the context
of algebra, automata, and logic. We present several proofs and several variants the
result, as well as applications.
Thomas Colcombet. “
Regular cost functions, Part I: logic and algebra over
words”. Log. Methods Comput. Sci., 2013, pages 47.
The theory of regular cost
functions is a quantitative extension to the classical notion of regularity.
A cost function associates to each input a non-negative integer value (or
infinity), as opposed to languages which only associate to each input the
two values ‘inside’ and ‘outside’. This theory is a continuation of the work
on distance automata and similar models. These models of automata have
been successfully used for solving the star-height problem, the finite power
property, the finite substitution problem, the relative inclusion star-height
problem and the boundedness problem for monadic-second order logic over
words. Our notion of regularity can be – as in the classical theory of regular
languages – equivalently defined in terms of automata, expressions, algebraic
recognisability, and by a variant of the monadic second-order logic. Those
equivalences are strict extensions of the corresponding classical results. The
present paper introduces the cost monadic logic, the quantitative extension
to the notion of monadic second-order logic we use, and show that some
problems of existence of bounds are decidable for this logic. This is achieved by
introducing the corresponding algebraic formalism: stabilisation monoids.
Thomas Colcombet and
Laure Daviaud. “
Approximate Comparison of Distance
Automata”. STACS 2013: 30th International Symposium on Theoretical
Aspects of Computer Science, 2013, pages 574-585. LIPIcs, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik. Editors
Natacha Portier and
Thomas Wilke.
Distance automata are automata weighted over the tropical semiring
.
Such automata compute functions from words to
. It is known that testing
is an undecidable
problem for
and
computed by distance automata. The main contribution of this paper is to show that
an approximation of this problem becomes decidable.
We present an algorithm which given
and
,
computed by distance automata answers ”yes” if
, ”no” if there is a
word w such that ,
and may answer ”yes” or ”no” in all other cases. This result highly refines previously
known decidability results of the same type.
The core argument behind this quasi-decision procedure is an algorithm which is
able to provide an approximated finite presentation to the closure under products of
sets of matrices over the tropical semiring. We also provide another theorem of
affine domination which shows that previously known decision procedures for
cost-automata have an improved precision when used over distance automata.
Thomas Colcombet. “
Composition with algebra at the background”. CSR 2013:
8th International Computer Science Symposium in Russia, 2013, pages 391-404. Lect.
Notes Comput. Sci., Springer.
Gurevich and Rabinovich raised the following
question: given a property of a set of rational numbers definable in the real line by
a monadic second-order formula, is it possible to define it directly in the
rational line? In other words, is it true that the presence of reals at the
background do not increase the expressive power of monadic second-order
logic?
In this paper, we answer positively this question. The proof in itself is a simple
application of classical and more recent techniques. This question will guide us in a
tour of results and ideas related to monadic theories of linear orderings.
Weakly definable languages of infinite trees are an expressive subclass of
regular tree languages definable in terms of weak monadic second-order logic, or
equivalently weak alternating automata. Our main result is that given a Büchi
automaton, it is decidable whether the language is weakly definable. We also show
that given a parity automaton, it is decidable whether the language is recognizable
by a nondeterministic co-Büchi automaton.
The decidability proofs build on recent results about cost automata over infinite
trees. These automata use counters to define functions from infinite trees to the
natural numbers extended with infinity. We reduce to testing whether the functions
defined by certain ”quasi-weak” cost automata are bounded by a finite value.
Thomas Colcombet. “
Cost Functions with Several Orders of Magnitudes and the
use of Relative Internal Set Theory”. LICS 2013: 28th Annual ACM/IEEE
Symposium on Logic in Computer Science, 2013, pages 123.
Cost monadic
logic extends monadic second-order logic with the ability to measure the cardinal of
sets. In particular, it allows to decide problems related to boundedness questions. In
this paper, we provide new decidability results allowing the systematic investigation
of questions involving “relative boundedness”. The first contribution in this work is
to introduce a suitable logic for such questions. The second is to show the
decidability of this logic over finite words. The third contribution is the use of
non-standard analysis: we advacate that developing the proofs in the axiomatic
system of “relative internal set theory” entails a significant simplification of the
proofs.
B-automata are
automata that can compute functions from words to non-negative integers or infinity.
In this paper we give another semantics to the hierarchical variant of these automata.
This new semantics is equivalent to the classical one in the terminology of cost
functions: functions computed are equivalent up to a polynomial factor. We provide
three applications of the technique.
Our first application shows that it is possible to evaluate, reading once the word
from left to right, in deterministic logspace, a B-automaton with the new
semantics. A similar evaluation would require polynomial space with the original
semantics.
Our second theorem shows that for games with hB-quantitative objectives, there
are positional determinacy strategies that are uniformly optimal, i.e., optimal from
any starting point.
Finally, we introduce a new form of history-determinism that is uniform in the
sense that translation strategies are independent from bounds. We show that
uniform history-determinism cannot be enforced for usual B-automata, and
we disclose new forms of (equivalent) automata that have this property.
Thomas Colcombet. “
Fonctions Régulières de Coût”. 2013. Note: Habilitation
thesis, in french.
This thesis gives a broad picture of the theory of
regular cost functions. Regular cost functions are quantitative extensions to regular
languages. A cost function is a function from words (or trees. . .) to the non-negative
integers or infinity. These functions are considered modulo an equivalence relation
that allows some distortion of the exact values, but preserves the existence of
bounds.
Regular cost functions form a sub-class that admits many effectively equivalent
charac- terisations in terms of logic, automata, algebra and regular expressions. Some
decidability results are deduced.
These results extend on the one hand the classical results on regular languages,
and on the other hand the works of Hashiguchi, Simon, Leung, and Kirsten
concerning distance automata, the tropical semiring and the star-height
problem.
This document describes the current knowledge about regular cost functions for
finite words, infinite words, finite trees and infinite trees.
2012
Thomas Colcombet. “
Forms of Determinism for Automata”. STACS 2012: 29th
International Symposium on Theoretical Aspects of Computer Science, 2012,
pages 1-23. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Editors
Christoph Dürr and
Thomas Wilke.
We survey in this
paper some variants of the notion of determinism, refining the spectrum
between non-determinism and determinism. We present unambiguous automata,
strongly unambiguous automata, prophetic automata, guidable automata, and
history-deterministic automata. We instantiate these various notions for finite
words, infinite words, finite trees, infinite trees, data languages, and cost
functions. The main results are underlined and some open problems proposed.
2011
Thomas Colcombet. “
Safra-like constructions for regular cost functions over
finite words”. 2011. Note: working paper or preprint.
Regular cost
functions have been introduced recently as an extension of the notion of
regular languages with counting capabilities, which retains strong closure,
equivalence, and decidability properties. Cost functions are functions ranging over
, and
considered modulo an equivalence which preserves the existence of bounds over each
subset of the domain. A central result in the theory of regular cost functions over
words is the duality theorem stating that the two dual forms of automata, namely
Band S-automata, are equivalent. The only known proof of this result relies on the
translation into an equivalent algebraic formalism. In this paper, we describe direct
translations from hierarchical B-automata to history-deterministic S-automata and
from hierarchical S-automata to history deterministic B-automata. We furthermore
describe how to optimize the number of counters of the output automaton, and how
to make them hierarchical. This construction is reminiscent of the famous
construction of Safra for the determinization of automata over infinite words.
We develop an algebraic model suitable for recognizing languages of words indexed
by countable linear orderings. We prove that this notion of recognizability is
effectively equivalent to definability in monadic second-order (MSO) logic. This
reproves in particular the decidability of MSO logic over the rationals with order.
Our proof also implies the first known collapse result for MSO logic over countable
linear orderings.
The notion of orbit finite data monoid was recently introduced by Bojanczyk as
an algebraic object for defining recognizable languages of data words.
In this paper, following Buchi’s approach, we introduce the new logic ”rigidly
guarded MSO” and show that the languages of data words definable in this logic are
exactly the languages recognizable by orbit finite data monoids.
We also establish, following this time the approach of Schutzenberger,
McNaughton and Papert, that the first-order variant of this logic exactly defines the
languages recognizable by aperiodic orbit finite data monoids.
Thomas Colcombet. “
Green’s Relations and their Use in Automata Theory”.
LATA 2011: Language and Automata Theory and Applications - 5th International
Conference, 2011, pages 1-21. Lect. Notes Comput. Sci., Springer. Editors
Adrian
Horia Dediu,
Shunsuke Inenaga, and Carlos Martin-Vide. Note: Invited lecture..
The objective of this survey is to present the ideal theory of monoids,
the so-called Green’s relations, and to illustrate the usefulness of this tool for
solving automata related questions. We use Green’s relations for proving four
classical results related to automata theory: The result of Schutzenberger
characterizing star-free languages, the theorem of factorization forests of Simon,
the characterization of infinite words of decidable monadic theory due to
Semenov, and the result of determinization of automata over infinite words of
Mc-Naughton.
2010
Thomas Colcombet,
Denis Kuperberg, and
Sylvain Lombardy. “
Regular
Temporal Cost Functions”. ICALP 2010 (2): Automata, Languages and
Programming, 37th International Colloquium, 2010, pages 563-574. Lect. Notes
Comput. Sci., Springer. Editors
Samson Abramsky,
Cyril Gavoille,
Claude Kirchner,
Friedhelm Meyer auf der Heide, and
Paul G. Spirakis.
Regular cost functions
have been introduced recently as an extension to the notion of regular languages with
counting capabilities, which retains strong closure, equivalence, and decidability
properties. The specificity of cost functions is that exact values are not considered,
but only estimated.
In this paper, we study the strict subclass of regular temporal cost functions. In
such cost functions, it is only allowed to count the number of occurrences of
consecutive events. For this reason, this model intends to measure the length
of intervals, i.e., a discrete notion of time. We provide various equivalent
representations for functions in this class, using automata, and ‘clock based’
reduction to regular language. We show that the conversions are much simpler to
obtain, and much more efficient than in the general case of regular cost
functions.
Our second aim in this paper is to use temporal cost function as a test-case for
exploring the algebraic nature of regular cost functions. Following the seminal ideas
of Schutzenberger, this results in a decidable algebraic characterization of
regular temporal cost functions inside the class of regular cost functions.
Thomas Colcombet and
Christof Löding. “
Regular cost functions over finite
trees”. LICS 2010: 5th Annual IEEE Symposium on Logic in Computer Science,
2010, pages 70-79. IEEE.
We develop the theory of regular cost functions over
finite trees: a quantitative extension to the notion of regular languages of
trees: Cost functions map each input (tree) to a value in omega + 1, and are
considered modulo an equivalence relation which forgets about specific values, but
preserves boundedness of functions on all subsets of the domain. We introduce
nondeterministic and alternating finite tree cost automata for describing cost
functions. We show that all these forms of automata are effectively equivalent.
We also provide decision procedures for them. Finally, follow- ing Büchi’s
seminal idea, we use cost automata for provid- ing decision procedures for cost
monadic logic, a quantita- tive extension of monadic second order logic.
Thomas Colcombet. “
Factorisation Forests for Infinite Words and applications to
countable scattered linear orderings”. Theor. Comput. Sci., 2010, pages 751–764.
Note: Selected papers of FCT 07.
The theorem of factorization forests of Imre
Simon shows the existence of nested factorizations — à la Ramsey — for finite
words. This theorem has important applications in semigroup theory, and
beyond.
We provide two improvements to the standard result. First we improve on all
previously known bounds. Second, we extend it to ‘every linear ordering’.
We use this last variant in a simplified proof of the translation of recognisable
languages over countable scattered linear orderings to languages accepted by
automata.
2009
Thomas Colcombet. “
The theory of stabilisation monoids and regular cost
functions”. ICALP 2009 (2): Automata, Languages and Programming, 36th
International Colloquium, 2009, pages 139–150. Lect. Notes Comput. Sci., Springer.
Editors
Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E.
Nikoletseas, and
Wolfgang Thomas.
We introduce the notion of regular
cost functions: a quantitative extension to the standard theory of regular languages.
We provide equivalent characterisations of this notion by means of automata
(extending the nested distance desert automata of Kirsten), of history-deterministic
automata (history-determinism is a weakening of the standard notion of determinism,
that replaces it in this context), and a suitable notion of recognisability
by stabilisation monoids. We also provide closure and decidability results.
Thomas Colcombet and
Konrad Zdanowski. “
A tight lower bound for
determinization of transition labeled Büchi automata”. ICALP 2009 (2):
Automata, Languages and Programming, 36th International Colloquium, 2009,
pages 151–162. Lect. Notes Comput. Sci., Springer. Editors
Susanne Albers,
Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and
Wolfgang Thomas.
In this paper we establish a lower bound
for the problem of translating a Büchi word automaton of
size
into a deterministic Rabin word automaton when both the Büchi
and the Rabin condition label transitions rather than states. This lower
bound exactly matches the known upper bound to this problem, namely
. Our
result entails a lower bound when the input Büchi automaton has (as it is usual) its
Büchi acceptance condition labeling states. Those lower bounds remain when the
output deterministic Rabin automaton has its Rabin acceptance condition labeling
states. Hence, in the standard setting, our result establishes a lower bound of
, while the best known
lower bound was .
A known upper bound in the standard setting is
.
Thomas Colcombet. “
Regular cost functions over words (draft)”. 2009. Note:
This is a draft, not reviewed. All the algebra part can be found with a better
presentation in the submitted ’Regular cost functions, Part I: logic and algebra over
words’.
We introduce and develop the notion of regular cost functions: a quantitative
extension to the standard theory of regular languages. This work is a continuation of
the works on distance automata and similar models. These models of automata have
been successfully used for solving the star-height problem, the finite power property,
the finite substitution problem, the relative inclusion star-height problem or the
boundedness problem for monadic-second order logic over words. Our notion of
regularity can be – as in the classical theory of regular languages – equivalently
defined in terms of automata, of algebraic recognisability, and by a variant of the
monadic second-order logic. Those equivalences are strict extensions of the
corresponding classical results. The decidability of the limitedness problem of
distance automata, as well as all its known variants can be deduced from our
results.
2008
Tree-walking automata are a natural sequential model for recognizing
tree languages. It is well known that every tree language recognized by a
tree-walking automaton is regular. We show that the converse does not hold.
Thomas Colcombet and
Christof Löding. “
The non-deterministic Mostowski
hierarchy and distance-parity automata”. ICALP 2008 (2): Automata, Languages
and Programming, 35th International Colloquium, 2008, pages 398–409. Lect. Notes
Comput. Sci., Springer. Editors
Luca Aceto, Ivan Damgård, Leslie Ann Goldberg,
Magnús M. Halldórsson,
Anna Ingólfsdóttir, and
Igor Walukiewicz.
Given
a Rabin tree-language and natural numbers i, j, the language is said to be
i,j-feasible if it is accepted by a parity automaton using priorities i,i+1,...,j. The
i,j-feasibility induces a hierarchy over the Rabin-tree languages called the
Mostowski hierarchy. In this paper we prove that the problem of deciding if a
language is i,j-feasible is reducible to the uniform universality problem for
distanceparity automata. Distance-parity automata form a new model of automata
extending both the nested distance desert automata introduced by Kirsten in his
proof of decidability of the star-height problem, and parity automata over
infinite trees. Distance-parity automata, instead of accepting a language,
attach to each tree a cost in omega+1. The uniform universality problem
consists in determining if this cost function is bounded by a finite value.
Thomas Colcombet and
Christof Löding. “
The nesting-depth of disjunctive
-calculus
for tree languages and the limitedness problem”. CSL 2008: 17th EACSL Annual
Conference on Computer Science Logic, 2008, pages 416–430. Lect. Notes Comput.
Sci., Springer. Editors Michael Kaminski and Simone Martini.
This chapter is
devoted to the presentation of the factorisation forest theorem, a deep result due to
Simon, which provides advanced Ramsey-like arguments in the context of algebra,
au- tomata, and logic. We present several proofs and several variants the result, as
well as applications.
We
survey operations on (possibly infinite) relational structures that are compatible
with logical theories in the sense that, if we apply the operation to given
structures then we can compute the theory of the resulting structure from the
theories of the arguments (the logics under consideration for the result and
the arguments might differ). Besides general compatibility results for these
operations we also present several results on restricted classes of structures, and
their use for obtaining classes of infinite structures with decidable theories.
2007
Thomas Colcombet. “
Factorisation forests for infinite words”. FCT 2007:
Fundamentals of Computation Theory, 16th International Symposium, 2007, pages
226–237. Lect. Notes Comput. Sci., Springer. Editors
Erzsébet Csuhaj-Varjú and
Zoltán Ésik.
The theorem of factorisation forests shows the existence of
nested factorisations — a la Ramsey — for finite words. This theorem has important
applications in semigroup theory, and beyond.
We provide two improvements to the standard result. First we improve on all
previously known bounds for the standard theorem. Second, we extend it to
every ‘complete linear ordering’. We use this variant in a simplified proof of
complementation of automata over words of countable scattered domain.
Following the idea developed by I. Simon in his theorem of Ramseyan
factorisation forests, we develop a result of ‘deterministic factorisations’. This
extra determinism property makes it usable on trees (finite or infinite). We
apply our result for proving that, over trees, every monadic interpretation is
equivalent to the composition of a first-order interpretation (with access to the
ancestor relation) and a monadic marking. Using this remark, we give new
characterisations for prefix-recognisable structures and for the Caucal hierarchy.
Furthermore, we believe that this approach has other potential applications.
The theorem of
factorisation forests shows the existence of nested factorisations — a la Ramsey —
for finite words. This theorem has important applications in semigroup theory, and
beyond. The purpose of this paper is to illustrate the importance of this approach in
the context of automata over infinite words and trees. We extend the theorem of
factorisation forest in two directions: we show that it is still valid for any word
indexed by a linear ordering; and we show that it admits a deterministic variant for
words indexed by well-orderings. A byproduct of this work is also an improvement on
the known bounds for the original result. We apply the first variant for giving a
simplified proof of the closure under complementation of rational sets of
words indexed by countable scattered linear orderings. We apply the second
variant in the analysis of monadic second-order logic over trees, yielding new
results on monadic interpretations over trees. Consequences of it are new
caracterisations of prefix-recognizable structures and of the Caucal hierarchy.
We consider a new kind of interpretation over relational structures: finite sets
interpretations. Those interpretations are defined by weak monadic second-order
(WMSO) formulas with free set variables. They transform a given structure
into a structure with a domain consisting of finite sets of elements of the
orignal structure. The definition of these interpretations directly implies that
they send structures with a decidable WMSO theory to structures with
a decidable first-order theory. In this paper, we investigate the expressive
power of such interpretations applied to infinite deterministic trees. The
results can be used in the study of automatic and tree-automatic structures.
2006
Tree-walking
automata are a natural sequential model for recognizing languages of finite trees.
Such automata walk around the tree and may decide in the end to accept it. It is
shown that deterministic tree-walking automata are weaker than nondeterministic
tree-walking automata.
Thomas Colcombet and
Damian Niwiński. “
On the positional determinacy of
edge-labeled games”. Theor. Comput. Sci., 2006, pages 190–196. Doi
10.1016/j.tcs.2005.10.046.
It is well known that games with the parity winning
condition admit positional determinacy : the winner has always a positional
(memoryless) strategy. This property continues to hold if edges rather than vertices
are labeled. We show that in this latter case the converse is also true. That is, a
winning condition over arbitrary set of colors admits positional determinacy in all
games if and only if it can be reduced to a parity condition with some finite number
of priorities.
We consider an extension of
-regular
expressions where two new variants of the Kleene star
are added:
and
. These
exponents act as the standard star, but restrict the number of iterations to be bounded (for
) or to tend toward
infinity (for
).
These expressions can define languages that are not omega-regular.
We develop a theory for these languages. We study the decidability and closure
questions. We also define an equivalent automaton model, extending Büchi
automata. This culminates with a — partial — complementation result.
We consider a new kind of interpretation over relational
structures: finite sets interpretations. Those interpretations are defined by weak
monadic second-order (WMSO) formulas with free set variables. They transform a
given structure into a structure with a domain consisting of finite sets of elements of
the orignal structure. The definition of these interpretations directly implies that
they send structures with a decidable WMSO theory to structures with
a decidable first-order theory. In this paper, we investigate the expressive
power of such interpretations applied to infinite deterministic trees. The
results can be used in the study of automatic and tree-automatic structures.
2005
Mikołaj Bojańczyk and
Thomas Colcombet. “
Tree-walking automata do not
recognize all regular languages”. STOC 2005: 37th Annual ACM Symposium on
Theory of Computing, 2005, pages 234–243. ACM.
Tree-walking automata are
a natural sequential model for recognizing tree languages. Every tree language
recognized by a tree-walking automaton is regular. In this paper, we present a tree
language which is regular but not recognized by any (nondeterministic) tree-walking
automaton. This settles a conjecture of Engelfriet, Hoogeboom and Van Best.
Moreover, the separating tree language is definable already in first-order logic
over a signature containing the left-son, right-son and ancestor relations.
2004
Tree-walking automata are a natural sequential model for recognizing tree
languages. It is shown that deterministic tree-walking automata are weaker than
nondeterministic tree-walking automata.
Thomas Colcombet and
Christof Löding. “
On the expressiveness of
deterministic transducers over infinite trees”. STACS 2004: 21st International
Symposium on Theoretical Aspects of Computer Science, 2004, pages 428–439. Lect.
Notes Comput. Sci., Springer. Editors
Volker Diekert and
Michel Habib.
We
introduce top-down deterministic transducers with rational lookahead (transducer
for short) working on infinite terms. We show that for such a transducer
, there exists an
MSO-transduction
such that for any graph ,
.
Reciprocally, we show that if an MSO-transduction
“preserves bisimilarity”, then there is a transducer
such that for
any graph ,
.
According to this, transducers can be seen as a complete method of implementation of
MSO-transductions that preserve bisimilarity. One application is for transformations
of equational systems.
Thomas Colcombet. “
Propriétés et représentation de structures infinies
(properties and representation of infinite structures)”. 2004.
This work is
dedicated to the study of infinite structures and graphs which admit a finite
representation, to their geometrical properties as well as decidability properties
concerning them. Following Courcelle’s work, we focus our study on their
representation as solution of equational systems.
We first introduce deterministic transducers (top-down with lookahead for
infinite trees). This tool allows us to deal with infinite equational systems,
thus extending some previous results, originally stated for finite equational
systems.
We then study the stack based families of structures and concentrate ourselves on
prefix recognizable ones. We establish various equivalent representations for them,
and study their restriction to bounded tree-width. We finally consider the enrichment
of those equational systems by an extra operator of fusion.
We then study structures admitting term-automatic presentations. We show once
more that those structures admit various equivalent representations.
Finally, we study the family of graphs definable by ground term rewriting and
establish some equivalences of representations. We conclude by a study of the nature
of those graphs when restricted to bounded tree or clique width.
Thomas Colcombet. “
Equational presentations of tree-automatic structures”.
WASL 04, 2004.
2003
Arnaud Carayol and
Thomas Colcombet. “
On equivalent representations of
infinite structures”. ICALP 2003: Automata, Languages and Programming, 30th
International Colloquium, 2003, pages 599–610. Lecture Notes in Comput. Sci.,
Springer. Editors Jos C. M. Baeten, Jan Karel Lenstra,
Joachim Parrow, and
Gerhard J. Woeginger.
According to Barthelman and Blumensath, the
following families of infinite graphs are isomorphic: (1) prefix-recognisable graphs, (2)
graph solutions of VR equational systems and (3) MS interpretations of regular trees.
In this paper, we consider the extension of prefix-recognisable graphs to
prefix-recognisable structures and of graphs solutions of VR equational systems to
structures solutions of positive quantifier free definable (PQFD) equational systems.
We extend Barthelman and Blumensath’s result to structures parameterised by
infinite graphs by proving that the following families of structures are equivalent: (1)
prefix-recognisable structures restricted by a language accepted by an infinite
deterministic automaton, (2) solutions of infinite PQFD equational systems and (3)
MS interpretations of the unfoldings of infinite deterministic graphs. Furthermore,
we show that the addition of a fuse operator, that merges several vertices
together, to PQFD equational systems does not increase their expressive power.
2002
We study the partial algebra of typed terms with an
associative commutative and idempotent operator (typed AC-terms). The originality
lies in the representation of the typing policy by a graph which has a decidable
monadic theory.
In this paper we show on two examples that some results on AC-terms can be
raised to the level of typed AC-terms. The examples are the results on rational
languages (in particular their closure by complement) and the property reachability
problem for ground rewrite systems (equivalently process rewrite systems).
Thomas Colcombet. “
On Families of Graphs Having a Decidable First Order
Theory with Reachability”. Automata, Languages and Programming, 29th
International Colloquium, ICALP 2002, 2002, pages 98–109. Lect. Notes
Comput. Sci., Springer. Editors Peter Widmayer, Francisco Ruiz Triguero,
Rafael Bueno Morales, Matthew Hennessy, Stephan Eidenbenz, and Ricardo
Conejo.
We consider a new class of infinite graphs defined as the
smallest solution of equational systems with vertex replacement operators and
unsynchronised product. We show that those graphs have an equivalent internal
representation as graphs of recognizable ground term rewriting systems.
Furthermore, we show that, when restricted to bounded tree-width, those graphs are
isomorphic to hyperedge replacement equational graphs. Finally, we prove that
on a wider family of graphs — interpretations of trees having a decidable
monadic theory — the first order theory with reachability is decidable.
2000
We propose an automatic
method to enforce trace properties on programs. The programmer specifies the
property separately from the program; a program transformer takes the program and
the property and automatically produces another “equivalent” pogram satisfying the
property. This separation of concerns makes the program easier to develop and
maintain. Our approach is both static and dynamic. It integrates static analyses in
order to avoid useless transformations. On the other hand, it never rejects
programs but adds dynamic checks when necessary. An important challenge is to
make this dynamic enforcement as inexpensive as possible. The most obvious
application domain is the enforcement of security policies. In particular, a
potential use of the method is the securization of mobile code upon receipt.