64 Search Results for "Colcombet, Thomas"

Document
DOI: 10.4230/LIPIcs.LICS.2026.24
Layered Automata: A Canonical Model for Automata over Infinite Words

Authors: Antonio Casares, Christof Löding, and Igor Walukiewicz

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that, for layered automata, both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.
Cite as

Antonio Casares, Christof Löding, and Igor Walukiewicz. Layered Automata: A Canonical Model for Automata over Infinite Words. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 24:1-24:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.LICS.2026.24,
  author =	{Casares, Antonio and L\"{o}ding, Christof and Walukiewicz, Igor},
  title =	{{Layered Automata: A Canonical Model for Automata over Infinite Words}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{24:1--24:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.24},
  URN =		{urn:nbn:de:0030-drops-268119},
  doi =		{10.4230/LIPIcs.LICS.2026.24},
  annote =	{Keywords: Omega automata, history determinism, canonical automata}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.30
The Uniformisation of Monadic Second-Order Logic over Countable Ordinals

Authors: Thomas Colcombet and Alexander Rabinovich

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains. Given a formula defining a relation between subsets of the input structure, the question is whether there exists a formula that defines a function selecting, for every set in the domain of the relation, a unique set such that the pair belongs to the relation. It is known, due to Lifsches and Shelah [Lifsches and Shelah, 1998], that MSO cannot, in general, be uniformised over the class of countable ordinals. We show that the maximal uniformisation degree is reached by extending the logic with a predicate that, given a set, selects (when possible) a cofinal subset of order type ω. Equivalently, every MSO formula can be uniformised over the class of countable ordinal chains using a formula in this extended logic.
Cite as

Thomas Colcombet and Alexander Rabinovich. The Uniformisation of Monadic Second-Order Logic over Countable Ordinals. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.LICS.2026.30,
  author =	{Colcombet, Thomas and Rabinovich, Alexander},
  title =	{{The Uniformisation of Monadic Second-Order Logic over Countable Ordinals}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{30:1--30:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.30},
  URN =		{urn:nbn:de:0030-drops-268178},
  doi =		{10.4230/LIPIcs.LICS.2026.30},
  annote =	{Keywords: Monadic second-order logic, uniformisation, chains, ordinals, composition method, factorization trees}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.73
A Cartesian Closed Fibration of Higher-Order Regular Languages

Authors: Paul-André Melliès and Vincent Moreau

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibrational techniques to derive the cartesian closed fibration from the various categories of regular languages of λ-terms associated to finite sets of ground states. In the second construction, we take advantage of the recent notion of profinite λ-calculus to define the cartesian closed fibration by a change-of-base from the fibration of clopen subsets over the category of Stone spaces, using an elegant idea coming from Hermida. We illustrate the expressive power of the cartesian closed fibration by generalizing the notion of Brzozowski derivative to higher-order regular languages, using an Isbell-like adjunction in the sense of Melliès and Zeilberger.
Cite as

Paul-André Melliès and Vincent Moreau. A Cartesian Closed Fibration of Higher-Order Regular Languages. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 73:1-73:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mellies_et_al:LIPIcs.LICS.2026.73,
  author =	{Melli\`{e}s, Paul-Andr\'{e} and Moreau, Vincent},
  title =	{{A Cartesian Closed Fibration of Higher-Order Regular Languages}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{73:1--73:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.73},
  URN =		{urn:nbn:de:0030-drops-268604},
  doi =		{10.4230/LIPIcs.LICS.2026.73},
  annote =	{Keywords: automata theory, categorical models and logics, logics of programs, programming language semantics}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2026.160
Gray Codes with Constant Delay and Constant Auxiliary Space

Authors: Antoine Amarilli, Claire David, Nadime Francis, Victor Marsault, Mikaël Monet, and Yann Strozecki

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Abstract
We give the first two algorithms to enumerate all binary words of {0,1}^𝓁 (like Gray codes) while ensuring that the delay and the auxiliary space is independent from 𝓁, i.e., constant time for each word, and constant memory in addition to the 𝓁 bits storing the current word. Our algorithms are given in two new computational models: tape machines and deque machines. We also study more restricted models, queue machines and stack machines, and show that they cannot enumerate all binary words with constant auxiliary space, even with unrestricted delay. A tape machine is a Turing machine that stores the current binary word on a single working tape of length 𝓁 (which never increases), using no other tape. The machine has a single head and must edit its tape to reach all possible words of {0,1}^𝓁, and output them (in unit time, by entering special output states), with no duplicates. Hence a tape machine uses constant auxiliary space by definition (up to the head position). We construct a tape machine that achieves this task with constant delay between consecutive outputs, so that the machine implements a so-called skew-tolerant quasi-Gray code. We then construct a more involved tape machine that implements a Gray code. A deque machine stores the current binary word on a double-ended queue of length 𝓁, and stores a constant-size internal state. It works as a tape machine, except that it modifies the content of the deque by performing push and pop operations on the endpoints. Hence again a deque machine uses constant auxiliary space by definition. We construct deque machines that enumerate all words of {0,1}^𝓁 with constant-delay. The main technical challenge in this model is to correctly detect when enumeration has finished.
Cite as

Antoine Amarilli, Claire David, Nadime Francis, Victor Marsault, Mikaël Monet, and Yann Strozecki. Gray Codes with Constant Delay and Constant Auxiliary Space. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 160:1-160:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.ICALP.2026.160,
  author =	{Amarilli, Antoine and David, Claire and Francis, Nadime and Marsault, Victor and Monet, Mika\"{e}l and Strozecki, Yann},
  title =	{{Gray Codes with Constant Delay and Constant Auxiliary Space}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{160:1--160:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.160},
  URN =		{urn:nbn:de:0030-drops-265485},
  doi =		{10.4230/LIPIcs.ICALP.2026.160},
  annote =	{Keywords: Gray code, Constant delay, Constant auxiliary space, Enumeration algorithms, Linear bounded automata, Tape machine, Deque machines, Counter implementation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2026.176
Expregular Functions

Authors: Thomas Colcombet, Nathan Lhote, and Pierre Ohlmann

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

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

Thomas Colcombet, Nathan Lhote, and Pierre Ohlmann. Expregular Functions. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 176:1-176:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2026.176,
  author =	{Colcombet, Thomas and Lhote, Nathan and Ohlmann, Pierre},
  title =	{{Expregular Functions}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{176:1--176:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.176},
  URN =		{urn:nbn:de:0030-drops-265647},
  doi =		{10.4230/LIPIcs.ICALP.2026.176},
  annote =	{Keywords: monadic second-order logic, exponential growth, automatic structures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2026.180
Optimally Controlling a Random Population

Authors: Hugo Gimbert, Corto Mascle, and Patrick Totzke

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Abstract
The population control problem is a parameterised problem where a controller sends messages to a whole population of identical finite-state agents, aiming to eventually move them all into a target state. The decision problem asks whether this can be achieved for arbitrarily large finite populations. We focus on the randomised version of this problem, where every agent is a copy of the same finite Markov Decision Process and non-determinism in the global action chosen by the controller is resolved independently and uniformly at random. Colcombet, Fijalkow and Ohlmann [Thomas Colcombet et al., 2021] showed that this problem is decidable, but without any complexity upper bound. We show that the random population control problem is in fact ExpTime-complete.
Cite as

Hugo Gimbert, Corto Mascle, and Patrick Totzke. Optimally Controlling a Random Population. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 180:1-180:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gimbert_et_al:LIPIcs.ICALP.2026.180,
  author =	{Gimbert, Hugo and Mascle, Corto and Totzke, Patrick},
  title =	{{Optimally Controlling a Random Population}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{180:1--180:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.180},
  URN =		{urn:nbn:de:0030-drops-265685},
  doi =		{10.4230/LIPIcs.ICALP.2026.180},
  annote =	{Keywords: Controller synthesis, Parameterized verification}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.63
Generalised Quantifiers Based on Rabin-Mostowski Index

Authors: Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these quantifiers. We study these problems in the realm of both ω-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of ω-words the new quantifiers can be effectively expressed in pure MSO logic. In contrast, in the case of infinite trees, addition of these quantifiers leads to an undecidable formalism. To realise index-quantifier elimination, we consider the extension of MSO by game quantifiers. As a tool, we provide a specific quantifier-elimination procedure for them. Moreover, we introduce a novel construction of transducers realising strategies in ω-regular games with monadic parameters.
Cite as

Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak. Generalised Quantifiers Based on Rabin-Mostowski Index. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 63:1-63:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.STACS.2026.63,
  author =	{Kuperberg, Denis and Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{Generalised Quantifiers Based on Rabin-Mostowski Index}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{63:1--63:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.63},
  URN =		{urn:nbn:de:0030-drops-255526},
  doi =		{10.4230/LIPIcs.STACS.2026.63},
  annote =	{Keywords: monadic quantifiers, decidability, quantifier elimination, parity automata, game quantifier, Rabin-Mostowski index}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.60
The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices

Authors: Stefan Kiefer and Andrew Ryzhikov

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We study finite semigroups of n × n matrices with rational entries. Such semigroups provide a rich generalization of transition monoids of unambiguous (and, in particular, deterministic) finite automata. In this paper we determine the maximum size of finite semigroups of rational n × n matrices, with the goal of shedding more light on the structure of such matrix semigroups. While in general such semigroups can be arbitrarily large in terms of n, a classical result of Schützenberger from 1962 implies an upper bound of 2^{𝒪(n² log n)} for irreducible semigroups, i.e., the only subspaces of ℚⁿ that are invariant for all matrices in the semigroup are ℚⁿ and the subspace consisting only of the zero vector. Irreducible matrix semigroups can be viewed as the building blocks of general matrix semigroups, and as such play an important role in mathematics and computer science. From the point of view of automata theory, they generalize strongly connected automata. Using a very different technique from that of Schützenberger, we improve the upper bound on the cardinality to 3^{n²}. This is the main result of the paper. The bound is in some sense tight, as we show that there exists, for every n, a finite irreducible semigroup with 3^{⌊ n²/4 ⌋} rational matrices. Our main result also leads to an improvement of a bound, due to Almeida and Steinberg, on the mortality threshold. The mortality threshold is a number 𝓁 such that if the zero matrix is in the semigroup, then the zero matrix can be written as a product of at most 𝓁 matrices from any subset that generates the semigroup.
Cite as

Stefan Kiefer and Andrew Ryzhikov. The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 60:1-60:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.STACS.2026.60,
  author =	{Kiefer, Stefan and Ryzhikov, Andrew},
  title =	{{The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{60:1--60:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.60},
  URN =		{urn:nbn:de:0030-drops-255496},
  doi =		{10.4230/LIPIcs.STACS.2026.60},
  annote =	{Keywords: finite matrix semigroups, irreducible matrix semigroups, matrix mortality, aperiodic semigroups, unambiguous automata, transition monoids}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.5
On the Complexity of Language Membership for Probabilistic Words

Authors: Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We study the membership problem to context-free languages L (CFLs) on probabilistic words, that specify for each position a probability distribution on the letters (assuming independence across positions). Our task is to compute, given a probabilistic word, what is the probability that a word drawn according to the distribution belongs to L. This problem generalizes the problem of counting how many words of length n belong to L, or of counting how many completions of a partial word belong to L. We show that this problem is in polynomial time for unambiguous context-free languages (uCFLs), but can be #P-hard already for unions of two linear uCFLs. More generally, we show that the problem is in polynomial time for so-called poly-slicewise-unambiguous languages, where given a length n we can tractably compute an uCFL for the words of length n in the language. This class includes some inherently ambiguous languages, and implies the tractability of bounded CFLs and of languages recognized by unambiguous polynomial-time counter automata; but we show that the problem can be #P-hard for nondeterministic counter automata, even for Parikh automata with a single counter. We then introduce classes of circuits from knowledge compilation which we use for tractable counting, and show that this covers the tractability of poly-slicewise-unambiguous languages and of some CFLs that are not poly-slicewise-unambiguous. Extending these circuits with negation further allows us to show tractability for the language of primitive words, and for the language of concatenations of two palindromes. We finally show the conditional undecidability of the meta-problem that asks, given a CFG, whether the probabilistic membership problem for that CFG is tractable or #P-hard.
Cite as

Antoine Amarilli, Mikaël Monet, Paul Raphaël, and Sylvain Salvati. On the Complexity of Language Membership for Probabilistic Words. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.STACS.2026.5,
  author =	{Amarilli, Antoine and Monet, Mika\"{e}l and Rapha\"{e}l, Paul and Salvati, Sylvain},
  title =	{{On the Complexity of Language Membership for Probabilistic Words}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{5:1--5:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.5},
  URN =		{urn:nbn:de:0030-drops-254943},
  doi =		{10.4230/LIPIcs.STACS.2026.5},
  annote =	{Keywords: Automaton, probabilistic words, context-free grammar, membership problem}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.2
Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

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

Abstract
Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.
Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.18
Complexity Landscape for Local Certification

Authors: Nicolas Bousquet, Laurent Feuilloley, and Sébastien Zeitoun

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
An impressive recent line of work has charted the complexity landscape of distributed graph algorithms. For many settings, it has been determined which time complexities exist, and which do not (in the sense that no local problem could have an optimal algorithm with that complexity). In this paper, we initiate the study of the landscape for space complexity of distributed graph algorithms. More precisely, we focus on the local certification setting, where a prover assigns certificates to nodes to certify a property, and where the space complexity is measured by the size of the certificates. Already for anonymous paths and cycles, we unveil a surprising landscape: - There is a gap between complexity O(1) and Θ(log log n) in paths. This is the first gap established in local certification. - There exists a property that has complexity Θ(log log n) in paths, a regime that was not known to exist for a natural property. - There is a gap between complexity O(1) and Θ(log n) in cycles, hence a gap that is exponentially larger than for paths. We then generalize our result for paths to the class of trees. Namely, we show that there is a gap between complexity O(1) and Θ(log log d) in trees, where d is the diameter. We finally describe some settings where there are no gaps at all. To prove our results we develop a new toolkit, based on various results of automata theory and arithmetic, which is of independent interest.
Cite as

Nicolas Bousquet, Laurent Feuilloley, and Sébastien Zeitoun. Complexity Landscape for Local Certification. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bousquet_et_al:LIPIcs.DISC.2025.18,
  author =	{Bousquet, Nicolas and Feuilloley, Laurent and Zeitoun, S\'{e}bastien},
  title =	{{Complexity Landscape for Local Certification}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{18:1--18:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.18},
  URN =		{urn:nbn:de:0030-drops-248350},
  doi =		{10.4230/LIPIcs.DISC.2025.18},
  annote =	{Keywords: Local certification, proof-labeling schemes, locally checkable proofs, space complexity, distributed graph algorithms, complexity gap}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2025.1
Lambdas, Transducers and MSO (Invited Talk)

Authors: Thomas Colcombet

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
This talk will revolve around the classical question: What kind of maps from words to words or trees to trees can be considered as "well behaved" from an automata theoretic point of view? What means to be well-behaved is left unspecified on purpose, but one thing is sure is that one would expect as minimal requirement that the inverse image of a regular language under such a map be effectively regular. One would also expect to have nice closure properties for these maps, in particular under composition. Ideally, we would also like to have several different equivalent computation models for representing them. This talk advertises the use of simply-typed lambda calculus as a good way to approach this question, and presents newer results concerning translations from and to exponential growth maps. This line of research is rooted in a long literature, starting from the works of Damm on higher order grammars, and the works of Engelfriet and Vogler on macro-tree transducers, and more generally from works on higher-order tree transducers, as well as the results of Ong et al. on decidability of MSO over higher-order recursion schemes (a model that produces infinite trees). These works show in a broad sense that models of computation defined in simply typed lambda-calculus do preserve regularity under taking the inverse image. Another connection is the recent implicit automata research programme initiated by Nguy~ên and Pradic, that was inspired by the seminal work of Hillebrand and Kanellakis. Here, automata models a directly viewed as programs written in some form of typed lambda-calculus, using Church encoding for representing inputs and outputs. When appropriately controlling the type system various it is possible to characterize various classes of finite state transducers studied in the literature. A last approach comes from finite model-theory. In this context, Monadic Second-Order Logic (MSO for short, the extension of first-order in which one can further quantify over sets) is the prime logic for describing regular languages over words or trees. This logic can also be used for defining transformations from words/trees to words/trees. These are the notions of MSO-interpretations or MSO-transducers. A major contribution here is the study of the expressive power of MSO-interpretations of polynomial growth from words to words that was undertaken by Bojańczyk, Kiefer and Lhote, and shown equivalent to other formalisms of transducers and programming languages. This is the class of polyregular functions, and it satisfies all the expectation of the question. Yet it is limited to finite words as inputs and outputs, and to polynomial growth. In a first part of the talk, we shall see how to use simply-typed lambda-calculus as a general mechanism for transforming trees into trees, and how it gives a positive answer to the original question. This description essentially repackages many ideas existing from the literature, in a way similar Gallot’s thesis. It also introduces a few new ones. In particular, we shall see generic results that some clearly identified classes of functional programs describing transformations from trees to trees can be effectively compiled into transducer-like models which perform only one pass on the input (i.e. higher-order tree transducers). This class of programs is also closed under composition. We shall also see how the logic MSO itself can be natively embedded in such models of computation. In a second part, we will see how this presentation relates to recent works with Lhote, Nguy~ên and Ohlmann in which extensions of polyregular functions to maps from words to words of exponential growth are studied. This work has the particularity to be the first one in the model-theoretic side of this theory in which it is key to allow lambda-terms to be unsafe.
Cite as

Thomas Colcombet. Lambdas, Transducers and MSO (Invited Talk). In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{colcombet:LIPIcs.MFCS.2025.1,
  author =	{Colcombet, Thomas},
  title =	{{Lambdas, Transducers and MSO}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip 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/LIPIcs.MFCS.2025.1},
  URN =		{urn:nbn:de:0030-drops-241087},
  doi =		{10.4230/LIPIcs.MFCS.2025.1},
  annote =	{Keywords: Lambda-calculus, automata theory, finite model theory, MSO}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.50
Lexicographic Transductions of Finite Words

Authors: Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Regular transductions over finite words have linear input-to-output growth. This class of transductions enjoys many characterizations, such as transductions computable by two-way transducers as well as transductions definable in MSO (in the sense of Courcelle). Recently, regular transductions have been extended by Bojańczyk to polyregular transductions, which have polynomial growth, and are characterized by pebble transducers and MSO interpretations. Another class of interest is that of transductions defined by streaming string transducers or marble transducers, which have exponential growth and are incomparable with polyregular transductions. In this paper, we consider MSO set interpretations (MSOSI) over finite words, that were introduced by Colcombet and Loeding. MSOSI are a natural candidate for the class of "regular transductions with exponential growth", and are rather well behaved. However, MSOSI for now lacks two desirable properties that regular and polyregular transductions have. The first property is to have an automata description. This property is closely related to a second property, that of being regularity preserving, meaning preserving regular languages under inverse image. We first show that if MSOSI are (effectively) regularity preserving then any automatic ω-word has a decidable MSO theory, an almost 20 years old conjecture of Bárány. Our main contribution is the introduction of a class of transductions of exponential growth, which we call lexicographic transductions. We provide three different presentations for this class: first, as the closure of simple transductions (recognizable transductions) under a single operator called maplex; second, as a syntactic fragment of MSOSI (but the regular languages are given by automata instead of formulas); and third, we give an automaton based model called nested marble transducers, which generalize both marble transducers and pebble transducers. We show that this class enjoys many nice properties including being regularity preserving.
Cite as

Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier. Lexicographic Transductions of Finite Words. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.MFCS.2025.50,
  author =	{Filiot, Emmanuel and Lhote, Nathan and Reynier, Pierre-Alain},
  title =	{{Lexicographic Transductions of Finite Words}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{50:1--50:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip 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/LIPIcs.MFCS.2025.50},
  URN =		{urn:nbn:de:0030-drops-241572},
  doi =		{10.4230/LIPIcs.MFCS.2025.50},
  annote =	{Keywords: Transducers, Automata, MSO, Logical interpretations, Automatic structures}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.64
Positional-Player Games

Authors: Orna Kupferman and Noam Shenwald

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
In reactive synthesis, we transform a specification to a system that satisfies the specification in all environments. For specifications in linear-temporal logic, research on bounded synthesis, where the sizes of the system and the environment are bounded, captures realistic settings and has lead to algorithms of improved complexity and implementability. In the game-based {a}pproach to synthesis, the system and its environment are modeled by strategies in a two-player game with an ω-regular objective, induced by the specification. There, bounded synthesis corresponds to bounding the memory of the strategies of the players. The memory requirement for various objectives has been extensively studied. In particular, researchers have identified positional objectives, where the winning player can follow a memoryless strategy - one that needs no memory. In this work we study bounded synthesis in the game setting. Specifically, we define and study positional-player games, in which one or both players are restricted to memoryless strategies, which correspond to non-intrusive control in various applications. We study positional-player games with Rabin, Streett, and Muller objectives, as well as with weighted multiple Büchi and reachability objectives. Our contribution covers their theoretical properties as well as a complete picture of the complexity of deciding the game in the various settings.
Cite as

Orna Kupferman and Noam Shenwald. Positional-Player Games. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 64:1-64:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.MFCS.2025.64,
  author =	{Kupferman, Orna and Shenwald, Noam},
  title =	{{Positional-Player Games}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{64:1--64:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip 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/LIPIcs.MFCS.2025.64},
  URN =		{urn:nbn:de:0030-drops-241719},
  doi =		{10.4230/LIPIcs.MFCS.2025.64},
  annote =	{Keywords: Games, \omega-Regular Objectives, Memory, Complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.66
Deciding Regular Games: a Playground for Exponential Time Algorithms

Authors: Zihui Liang, Bakh Khoussainov, and Mingyu Xiao

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Regular games form a well-established class of games for analysis and synthesis of reactive systems. They include colored Muller games, McNaughton games, Muller games, Rabin games, and Streett games. These games are played on directed graphs G where Player 0 and Player 1 play by generating an infinite path ρ through the graph. The winner is determined by specifications put on the set X of vertices in ρ that occur infinitely often. These games are determined, enabling the partitioning of G into two sets Win₀ and Win₁ of winning positions for Player 0 and Player 1, respectively. Numerous algorithms exist that decide instances of regular games, e.g., Muller games, by computing Win₀ and Win₁. In this paper we aim to find general principles for designing uniform algorithms that decide all regular games. For this we utilize various recursive and dynamic programming algorithms that leverage standard notions such as subgames and traps. Importantly, we show that our techniques improve or match the performances of existing algorithms for many instances of regular games.
Cite as

Zihui Liang, Bakh Khoussainov, and Mingyu Xiao. Deciding Regular Games: a Playground for Exponential Time Algorithms. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 66:1-66:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liang_et_al:LIPIcs.MFCS.2025.66,
  author =	{Liang, Zihui and Khoussainov, Bakh and Xiao, Mingyu},
  title =	{{Deciding Regular Games: a Playground for Exponential Time Algorithms}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{66:1--66:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip 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/LIPIcs.MFCS.2025.66},
  URN =		{urn:nbn:de:0030-drops-241732},
  doi =		{10.4230/LIPIcs.MFCS.2025.66},
  annote =	{Keywords: Regular games, colored Muller games, Rabin games, McNaughton games, Muller games, deciding games}
}
  • Refine by Type
  • 64 Document/PDF
  • 29 Document/HTML

  • Refine by Publication Year
  • 9 2026
  • 27 2025
  • 2 2024
  • 1 2023
  • 5 2022
  • Show More...

  • Refine by Author
  • 26 Colcombet, Thomas
  • 6 Casares, Antonio
  • 6 Kuperberg, Denis
  • 5 Lehtinen, Karoliina
  • 4 Manuel, Amaldev
  • Show More...

  • Refine by Series/Journal
  • 63 LIPIcs
  • 1 DagRep

  • Refine by Classification
  • 11 Theory of computation → Regular languages
  • 10 Theory of computation → Formal languages and automata theory
  • 9 Theory of computation → Logic and verification
  • 9 Theory of computation → Tree languages
  • 8 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 4 decidability
  • 3 Automata
  • 3 MSO
  • 3 Tree automata
  • 3 automata theory
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact