Document

**Published in:** LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

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.

Thomas Colcombet and Arthur Jaquard. A Complexity Approach to Tree Algebras: the Polynomial Case. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 37:1-37:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.MFCS.2022.37, author = {Colcombet, Thomas and Jaquard, Arthur}, title = {{A Complexity Approach to Tree Algebras: the Polynomial Case}}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)}, pages = {37:1--37:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-256-3}, ISSN = {1868-8969}, year = {2022}, volume = {241}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.37}, URN = {urn:nbn:de:0030-drops-168357}, doi = {10.4230/LIPIcs.MFCS.2022.37}, annote = {Keywords: Tree algebra, nominal automata, language theory} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

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.

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. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 117:1-117:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2022.117, author = {Casares, Antonio and Colcombet, Thomas and Lehtinen, Karoliina}, title = {{On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {117:1--117:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.117}, URN = {urn:nbn:de:0030-drops-164580}, doi = {10.4230/LIPIcs.ICALP.2022.117}, annote = {Keywords: Infinite duration games, Muller games, Rabin conditions, omega-regular languages, memory in games, good-for-games automata} }

Document

**Published in:** Dagstuhl Reports, Volume 11, Issue 10 (2022)

This report documents the program and the outcomes of Dagstuhl Seminar 21452 "Unambiguity in Automata Theory". The aim of the seminar was to improve the understanding of the notion of unambiguity in automata theory, especially with respect to questions related to the expressive power, succinctness, and the tractability of unambiguous devices. The main motivation behind these studies is the hope that unambiguous machines can provide a golden balance between efficiency - sometimes not worse than for deterministic devices - and expressibility / succinctness, which often is similar to the general nondeterministic machines. These trade-offs become especially important in the models where the expressiveness or the decidability status of unambiguous machines is different from that of nondeterministic ones, as it is the case, e.g., for register automata.

Thomas Colcombet, Karin Quaas, and Michał Skrzypczak. Unambiguity in Automata Theory (Dagstuhl Seminar 21452). In Dagstuhl Reports, Volume 11, Issue 10, pp. 57-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{colcombet_et_al:DagRep.11.10.57, author = {Colcombet, Thomas and Quaas, Karin and Skrzypczak, Micha{\l}}, title = {{Unambiguity in Automata Theory (Dagstuhl Seminar 21452)}}, pages = {57--71}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2022}, volume = {11}, number = {10}, editor = {Colcombet, Thomas and Quaas, Karin and Skrzypczak, Micha{\l}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.10.57}, URN = {urn:nbn:de:0030-drops-159282}, doi = {10.4230/DagRep.11.10.57}, annote = {Keywords: Unambiguity in Automata Theory, Dagstuhl Seminar} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

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.

Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal Transformations of Games and Automata Using Muller Conditions. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2021.123, author = {Casares, Antonio and Colcombet, Thomas and Fijalkow, Nathana\"{e}l}, title = {{Optimal Transformations of Games and Automata Using Muller Conditions}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {123:1--123:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.123}, URN = {urn:nbn:de:0030-drops-141928}, doi = {10.4230/LIPIcs.ICALP.2021.123}, annote = {Keywords: Automata over infinite words, Omega regular languages, Determinisation of automata} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

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.

Thomas Colcombet and Arthur Jaquard. A Complexity Approach to Tree Algebras: the Bounded Case. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 127:1-127:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2021.127, author = {Colcombet, Thomas and Jaquard, Arthur}, title = {{A Complexity Approach to Tree Algebras: the Bounded Case}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {127:1--127:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.127}, URN = {urn:nbn:de:0030-drops-141966}, doi = {10.4230/LIPIcs.ICALP.2021.127}, annote = {Keywords: Tree algebra, infinite tree, language theory} }

Document

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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.

Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. Learning Automata and Transducers: A Categorical Approach. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CSL.2021.15, author = {Colcombet, Thomas and Petri\c{s}an, Daniela and Stabile, Riccardo}, title = {{Learning Automata and Transducers: A Categorical Approach}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.15}, URN = {urn:nbn:de:0030-drops-134498}, doi = {10.4230/LIPIcs.CSL.2021.15}, annote = {Keywords: Automata, transducer, learning, category} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

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 λY-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.

David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys. Cost Automata, Safe Schemes, and Downward Closures. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 109:1-109:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barozzini_et_al:LIPIcs.ICALP.2020.109, author = {Barozzini, David and Clemente, Lorenzo and Colcombet, Thomas and Parys, Pawe{\l}}, title = {{Cost Automata, Safe Schemes, and Downward Closures}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {109:1--109:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.109}, URN = {urn:nbn:de:0030-drops-125169}, doi = {10.4230/LIPIcs.ICALP.2020.109}, annote = {Keywords: Cost logics, cost automata, downward closures, higher-order recursion schemes, safe recursion schemes} }

Document

**Published in:** LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

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 ⩽ g, there exists effectively an unambiguous tropical automaton computing h such that f ⩽ h ⩽ 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.

Thomas Colcombet and Sylvain Lombardy. Unambiguous Separators for Tropical Tree Automata. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 32:1-32:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2020.32, author = {Colcombet, Thomas and Lombardy, Sylvain}, title = {{Unambiguous Separators for Tropical Tree Automata}}, booktitle = {37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)}, pages = {32:1--32:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-140-5}, ISSN = {1868-8969}, year = {2020}, volume = {154}, editor = {Paul, Christophe and Bl\"{a}ser, Markus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.32}, URN = {urn:nbn:de:0030-drops-118933}, doi = {10.4230/LIPIcs.STACS.2020.32}, annote = {Keywords: Tree automata, Tropical semiring, Separation, Unambiguity} }

Document

Track A: Algorithms, Complexity and Games

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

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, Joël Ouaknine, Pavel Semukhin, and James Worrell. On Reachability Problems for Low-Dimensional Matrix Semigroups. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 44:1-44:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2019.44, author = {Colcombet, Thomas and Ouaknine, Jo\"{e}l and Semukhin, Pavel and Worrell, James}, title = {{On Reachability Problems for Low-Dimensional Matrix Semigroups}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {44:1--44:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.44}, URN = {urn:nbn:de:0030-drops-106209}, doi = {10.4230/LIPIcs.ICALP.2019.44}, annote = {Keywords: membership problem, half-space reachability problem, matrix semigroups, Heisenberg group, general linear group} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

In this paper we adopt a category-theoretic approach to the conception of automata classes enjoying minimization by design. The main instantiation of our construction is a new class of automata that are hybrid between deterministic automata and automata weighted over a field.

Thomas Colcombet and Daniela Petrisan. Automata in the Category of Glued Vector Spaces. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.MFCS.2017.52, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata in the Category of Glued Vector Spaces}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {52:1--52:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.52}, URN = {urn:nbn:de:0030-drops-81324}, doi = {10.4230/LIPIcs.MFCS.2017.52}, annote = {Keywords: hybrid set-vector automata, automata minimization in a category} }

Document

**Published in:** LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

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 applied to several phenomena in automata theory, starting with determinization and
minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to
Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.

Thomas Colcombet and Daniela Petrisan. Automata Minimization: a Functorial Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CALCO.2017.8, author = {Colcombet, Thomas and Petrisan, Daniela}, title = {{Automata Minimization: a Functorial Approach}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.8}, URN = {urn:nbn:de:0030-drops-80484}, doi = {10.4230/LIPIcs.CALCO.2017.8}, annote = {Keywords: functor automata, minimization, Choffrut's minimization algorithm, subsequential transducers, Brzozowski's minimization algorithm} }

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

In this paper, we exhibit a one-to-one correspondence between omega-regular languages and a subclass of regular cost functions over finite words, called omega-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 a simple description of an optimal procedure of history-determinisation for cost automata, a central result in the theory of regular cost functions.

Thomas Colcombet and Nathanaël Fijalkow. The Bridge Between Regular Cost Functions and Omega-Regular Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 126:1-126:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2016.126, author = {Colcombet, Thomas and Fijalkow, Nathana\"{e}l}, title = {{The Bridge Between Regular Cost Functions and Omega-Regular Languages}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {126:1--126:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.126}, URN = {urn:nbn:de:0030-drops-62619}, doi = {10.4230/LIPIcs.ICALP.2016.126}, annote = {Keywords: Theory of Regular Cost Functions, Automata with Counters, Costautomata, Quantitative Extensions of Automata, Determinisation of Automata} }

Document

**Published in:** LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

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 "exists t forall s exists r: phi(r,s,t)", where phi does not use quantifiers over number variables, and variables r and s can be only used simultaneously, in subformulae of the form s < f(x) <= r.

Achim Blumensath, Thomas Colcombet, and Pawel Parys. On a Fragment of AMSO and Tiling Systems. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{blumensath_et_al:LIPIcs.STACS.2016.19, author = {Blumensath, Achim and Colcombet, Thomas and Parys, Pawel}, title = {{On a Fragment of AMSO and Tiling Systems}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {19:1--19:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.19}, URN = {urn:nbn:de:0030-drops-57202}, doi = {10.4230/LIPIcs.STACS.2016.19}, annote = {Keywords: monadic second-order logic, boundedness, tiling problems} }

Document

**Published in:** LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

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.

Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Torunczyk. Cost Functions Definable by Min/Max Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2016.29, author = {Colcombet, Thomas and Kuperberg, Denis and Manuel, Amaldev and Torunczyk, Szymon}, title = {{Cost Functions Definable by Min/Max Automata}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {29:1--29:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.29}, URN = {urn:nbn:de:0030-drops-57305}, doi = {10.4230/LIPIcs.STACS.2016.29}, annote = {Keywords: distance automata, B-automata, regular cost functions, stabilisation monoids, decidability, min-automata, max-automata} }

Document

**Published in:** LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

We study fragments of a mu-calculus over data words whose primary modalities are 'go to next position' (X^g), 'go to previous position}' (Y^g), 'go to next position with the same data value' (X^c), 'go to previous position with the same data value (Y^c)'. Our focus is on two fragments that are called the bounded mode
alternation fragment (BMA) and the bounded reversal fragment (BR). BMA is the fragment of those formulas that whose unfoldings contain only a bounded number of alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Similarly BR is the fragment of formulas whose unfoldings contain only a bounded number of alternations between left modalities (Y^g, Y^c) and right modalities (X^g, X^c). We show that these fragments are decidable (by inclusion in Data Automata), enjoy effective Boolean closure, and contain previously defined logics such as the two variable fragment of first-order logic and DataLTL. More precisely the definable language in each formalism obey the following inclusions that are effective.
FO^2 subsetneq DataLTL subsetneq BMA BR subsetneq nu subseteq Data Automata.
Our main contribution is a method to prove inexpressibility results on the fragment BMA by reducing them to inexpressibility results for combinatorial expressions. More precisely we prove the following hierarchy of definable languages,
emptyset=BMA^0 subsetneq BMA^1 subsetneq ... subsetneq BMA subsetneq BR , where BMA^k is the set of all formulas whose unfoldings contain at most k-1 alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Since the class BMA is a generalization of FO^2 and DataLTL the inexpressibility results carry over to them as well.

Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 98-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2015.98, author = {Colcombet, Thomas and Manuel, Amaldev}, title = {{Fragments of Fixpoint Logic on Data Words}}, booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)}, pages = {98--111}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-97-2}, ISSN = {1868-8969}, year = {2015}, volume = {45}, editor = {Harsha, Prahladh and Ramalingam, G.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.98}, URN = {urn:nbn:de:0030-drops-56289}, doi = {10.4230/LIPIcs.FSTTCS.2015.98}, annote = {Keywords: Data words, Data automata, Fixpoint logic} }

Document

**Published in:** LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

A new paradigm, called combinatorial expressions, for computing functions expressing properties over 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. Some extensions and normal forms are also presented.

Thomas Colcombet and Amaldev Manuel. Combinatorial Expressions and Lower Bounds. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 249-261, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2015.249, author = {Colcombet, Thomas and Manuel, Amaldev}, title = {{Combinatorial Expressions and Lower Bounds}}, booktitle = {32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)}, pages = {249--261}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-78-1}, ISSN = {1868-8969}, year = {2015}, volume = {30}, editor = {Mayr, Ernst W. and Ollinger, Nicolas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.249}, URN = {urn:nbn:de:0030-drops-49181}, doi = {10.4230/LIPIcs.STACS.2015.249}, annote = {Keywords: expressions, lower bound, indefinability} }

Document

**Published in:** LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Data omega-words are omega-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 omega-words and it is shown that the mu-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.

Thomas Colcombet and Amaldev Manuel. Generalized Data Automata and Fixpoint Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 267-278, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.267, author = {Colcombet, Thomas and Manuel, Amaldev}, title = {{Generalized Data Automata and Fixpoint Logic}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {267--278}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-77-4}, ISSN = {1868-8969}, year = {2014}, volume = {29}, editor = {Raman, Venkatesh and Suresh, S. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.267}, URN = {urn:nbn:de:0030-drops-48483}, doi = {10.4230/LIPIcs.FSTTCS.2014.267}, annote = {Keywords: Data words, Data Automata, Decidability, Fixpoint Logic} }

Document

**Published in:** LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

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 positional strategies in games with counters.

Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.379, author = {Colcombet, Thomas and Fijalkow, Nathanael and Horn, Florian}, title = {{Playing Safe}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {379--390}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-77-4}, ISSN = {1868-8969}, year = {2014}, volume = {29}, editor = {Raman, Venkatesh and Suresh, S. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.379}, URN = {urn:nbn:de:0030-drops-48571}, doi = {10.4230/LIPIcs.FSTTCS.2014.379}, annote = {Keywords: Game Theory, Synthesis, Safety Specifications, Program Verification} }

Document

**Published in:** LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

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, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 215-230, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.CSL.2013.215, author = {Colcombet, Thomas and Kuperberg, Denis and L\"{o}ding, Christof and Vanden Boom, Michael}, title = {{Deciding the weak definability of B\"{u}chi definable tree languages}}, booktitle = {Computer Science Logic 2013 (CSL 2013)}, pages = {215--230}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-60-6}, ISSN = {1868-8969}, year = {2013}, volume = {23}, editor = {Ronchi Della Rocca, Simona}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.215}, URN = {urn:nbn:de:0030-drops-41998}, doi = {10.4230/LIPIcs.CSL.2013.215}, annote = {Keywords: Tree automata, weak definability, decidability, cost automata, boundedness} }

Document

**Published in:** LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

Distance automata are automata weighted over the semiring (\mathbb{N} \cup \infty,\min,+) (the tropical semiring). Such automata compute functions from words to \mathbb{N} \cup \infty such as the number of occurrences of a given letter. It is known that testing f <= g is an undecidable problem for f,g 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 epsilon > 0 and two functions f,g computed by distance automata, answers "yes" if f <= (1-epsilon) g, "no" if $f \not\leq g$, 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 and Laure Daviaud. Approximate comparison of distance automata. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 574-585, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2013.574, author = {Colcombet, Thomas and Daviaud, Laure}, title = {{Approximate comparison of distance automata}}, booktitle = {30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)}, pages = {574--585}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-50-7}, ISSN = {1868-8969}, year = {2013}, volume = {20}, editor = {Portier, Natacha and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.574}, URN = {urn:nbn:de:0030-drops-39667}, doi = {10.4230/LIPIcs.STACS.2013.574}, annote = {Keywords: Distance automata, tropical semiring, decidability, cost functions} }

Document

Invited Talk

**Published in:** LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

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.

Thomas Colcombet. Forms of Determinism for Automata (Invited Talk). In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{colcombet:LIPIcs.STACS.2012.1, author = {Colcombet, Thomas}, title = {{Forms of Determinism for Automata}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {1--23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-35-4}, ISSN = {1868-8969}, year = {2012}, volume = {14}, editor = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.1}, URN = {urn:nbn:de:0030-drops-33862}, doi = {10.4230/LIPIcs.STACS.2012.1}, annote = {Keywords: Automata, determinism, unambiguity, words, infinite trees} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail