17 Search Results for "Carayol, Arnaud"

Document
DOI: 10.4230/LIPIcs.STACS.2026.31
Lower Bounds for Ranking-Based Pivot Rules

Authors: Yann Disser, Georg Loho, Matthew Maat, and Nils Mosis

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

Abstract
The existence of a polynomial pivot rule for the simplex method for linear programming, policy iteration for Markov decision processes, and strategy improvement for parity games each are prominent open problems in their respective fields. While numerous natural candidates for efficient rules have been eliminated, all existing lower bound constructions are tailored to individual or small sets of pivot rules. We introduce a unified framework for formalizing classes of rules according to the information about the input that they rely on. Within this framework, we show lower bounds for ranking-based classes of rules that base their decisions on orderings of the improving pivot steps induced by the underlying data. Our first result is a superpolynomial lower bound for strategy improvement, obtained via a family of sink parity games, which applies to memory-based generalizations of Bland’s rule that only access the input by comparing the ranks of improving edges in some global order. Our second result is a subexponential lower bound for policy iteration, obtained via a family of Markov decision processes, which applies to memoryless rules that only access the input by comparing improving actions according to their ranks in a global order, their reduced costs, and the associated improvements in objective value. Both results carry over to the simplex method for linear programming.
Cite as

Yann Disser, Georg Loho, Matthew Maat, and Nils Mosis. Lower Bounds for Ranking-Based Pivot Rules. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{disser_et_al:LIPIcs.STACS.2026.31,
  author =	{Disser, Yann and Loho, Georg and Maat, Matthew and Mosis, Nils},
  title =	{{Lower Bounds for Ranking-Based Pivot Rules}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{31:1--31:19},
  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.31},
  URN =		{urn:nbn:de:0030-drops-255207},
  doi =		{10.4230/LIPIcs.STACS.2026.31},
  annote =	{Keywords: lower bounds, Markov decision processes, parity games, pivot rules, policy iteration, simplex method}
}
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.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

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

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  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.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.31
Games with ω-Automatic Preference Relations

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

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

Abstract
This paper investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as ω-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an ω-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. When a (constrained) NE exists, we show that there always exists one with finite-memory strategies. Finally, we explore fundamental properties of ω-automatic relations and their implications in the existence of equilibria.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. Games with ω-Automatic Preference Relations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.MFCS.2025.31,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{Games with \omega-Automatic Preference Relations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{31:1--31: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.31},
  URN =		{urn:nbn:de:0030-drops-241381},
  doi =		{10.4230/LIPIcs.MFCS.2025.31},
  annote =	{Keywords: Games played on graphs, Nash equilibrium, \omega-automatic relations, \omega-recognizable relations, constrained Nash equilibria existence problem}
}
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}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.7
Temporal Explorability Games

Authors: Pete Austin, Sougata Bose, Nicolas Mazzocchi, and Patrick Totzke

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Temporal graphs extend ordinary graphs with discrete time that affects the availability of edges. We consider solving games played on temporal graphs where one player aims to explore the graph, i.e., visit all vertices. The complexity depends majorly on two factors: the presence of an adversary and how edge availability is specified. We demonstrate that on static graphs, where edges are always available, solving explorability games is just as hard as solving reachability games. In contrast, on temporal graphs, the complexity of explorability coincides with generalized reachability (NP-complete for one-player and PSPACE-complete for two player games). We show that if temporal graphs are given symbolically, even one-player reachability (and thus explorability and generalized reachability) games are PSPACE-hard. For one player, all these are also solvable in PSPACE and for two players, they are in PSPACE, EXP and EXP, respectively.
Cite as

Pete Austin, Sougata Bose, Nicolas Mazzocchi, and Patrick Totzke. Temporal Explorability Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{austin_et_al:LIPIcs.CONCUR.2025.7,
  author =	{Austin, Pete and Bose, Sougata and Mazzocchi, Nicolas and Totzke, Patrick},
  title =	{{Temporal Explorability Games}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.7},
  URN =		{urn:nbn:de:0030-drops-239575},
  doi =		{10.4230/LIPIcs.CONCUR.2025.7},
  annote =	{Keywords: Temporal Graphs, Explorability, Reachability, Games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.138
Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Authors: Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter MDPs (OC-MDPs). They extend finite MDPs via an associated counter taking natural values, thus inducing an infinite MDP over the set of configurations (current state and counter value). We consider two characteristic objectives: reaching a target state (state-reachability), and reaching a target state with counter value zero (selective termination). The synthesis problem for the latter is not known to be decidable and connected to major open problems in number theory. Furthermore, even seemingly simple strategies (e.g., memoryless ones) in OC-MDPs might be impossible to build in practice (due to the underlying infinite configuration space): we need finite, and preferably small, representations. To overcome these obstacles, we introduce two natural classes of concisely represented strategies based on a (possibly infinite) partition of counter values in intervals. For both classes, and both objectives, we study the verification problem (does a given strategy ensure a high enough probability for the objective?), and two synthesis problems (does there exist such a strategy?): one where the interval partition is fixed as input, and one where it is only parameterized. We develop a generic approach based on a compression of the induced infinite MDP that yields decidability in all cases, with all complexities within PSPACE.
Cite as

Michal Ajdarów, James C. A. Main, Petr Novotný, and Mickael Randour. Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 138:1-138:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ajdarow_et_al:LIPIcs.ICALP.2025.138,
  author =	{Ajdar\'{o}w, Michal and Main, James C. A. and Novotn\'{y}, Petr and Randour, Mickael},
  title =	{{Taming Infinity One Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{138:1--138:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l 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.2025.138},
  URN =		{urn:nbn:de:0030-drops-235157},
  doi =		{10.4230/LIPIcs.ICALP.2025.138},
  annote =	{Keywords: one-counter Markov decision processes, randomised strategies, termination, reachability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.155
Approximate Problems for Finite Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Finite (word) state transducers extend finite state automata by defining a binary relation over finite words, called rational relation. If the rational relation is the graph of a function, this function is said to be rational. The class of sequential functions is a strict subclass of rational functions, defined as the functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems and show they are decidable as well. This includes the approximate functionality problem, which asks whether given a rational relation (by a transducer), is it close to a rational function, and the approximate determinisation problem, which asks whether a given rational function is close to a sequential function. We prove decidability results for several classical distances, including Hamming and Levenshtein edit distance. Finally, we investigate the approximate uniformisation problem, which asks, given a rational relation R, whether there exists a sequential function that is close to some function uniformising R. As its exact version, we prove that this problem is undecidable.
Cite as

Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny. Approximate Problems for Finite Transducers. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 155:1-155:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2025.155,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and Madnani, Khushraj and Sunny, Saina},
  title =	{{Approximate Problems for Finite Transducers}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{155:1--155:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l 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.2025.155},
  URN =		{urn:nbn:de:0030-drops-235329},
  doi =		{10.4230/LIPIcs.ICALP.2025.155},
  annote =	{Keywords: Finite state transducers, Edit distance, Determinisation, Functionality}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.69
A Dichotomy Theorem for Ordinal Ranks in MSO

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

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We focus on formulae ∃X.φ(Y, X) of monadic second-order logic over the full binary tree, such that the witness X is a well-founded set. The ordinal rank rank(X) < ω₁ of such a set X measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula φ. Let η_φ be the minimal ordinal such that, whenever an instance Y satisfies the formula, there is a witness X with rank(X) ≤ η_φ. Then η_φ is either strictly smaller than ω² or it reaches the maximal possible value ω₁. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
Cite as

Damian Niwiński, Paweł Parys, and Michał Skrzypczak. A Dichotomy Theorem for Ordinal Ranks in MSO. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 69:1-69:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{niwinski_et_al:LIPIcs.STACS.2025.69,
  author =	{Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{A Dichotomy Theorem for Ordinal Ranks in MSO}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{69:1--69:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine 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.2025.69},
  URN =		{urn:nbn:de:0030-drops-228942},
  doi =		{10.4230/LIPIcs.STACS.2025.69},
  annote =	{Keywords: dichotomy result, limit ordinal, countable ordinals, nondeterministic tree automata}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.131
The Structure of Trees in the Pushdown Hierarchy

Authors: Arnaud Carayol and Lucien Charamond

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
In this article, we investigate the structure of the trees in the pushdown hierarchy, a hierarchy of infinite graphs having a decidable MSO-theory. We show that a binary complete tree in the pushdown hierarchy must contain at least two different subtrees which are isomorphic. We extend this property to any tree with no leaves and with chains of unary vertices of bounded length. We provided two applications of this result. A first application in formal language theory, gives a simple argument to show that some languages are not deterministic higher-order indexed languages. A second application in number theory shows that the real numbers defined by deterministic higher-order pushdown automata are either rational or transcendental.
Cite as

Arnaud Carayol and Lucien Charamond. The Structure of Trees in the Pushdown Hierarchy. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 131:1-131:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.ICALP.2024.131,
  author =	{Carayol, Arnaud and Charamond, Lucien},
  title =	{{The Structure of Trees in the Pushdown Hierarchy}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{131:1--131:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.131},
  URN =		{urn:nbn:de:0030-drops-202749},
  doi =		{10.4230/LIPIcs.ICALP.2024.131},
  annote =	{Keywords: Pushdown hierarchy, Monadic second-order logic, Automatic numbers}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.19
One Drop of Non-Determinism in a Random Deterministic Automaton

Authors: Arnaud Carayol, Philippe Duchon, Florent Koechlin, and Cyril Nicaud

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
Every language recognized by a non-deterministic finite automaton can be recognized by a deterministic automaton, at the cost of a potential increase of the number of states, which in the worst case can go from n states to 2ⁿ states. In this article, we investigate this classical result in a probabilistic setting where we take a deterministic automaton with n states uniformly at random and add just one random transition. These automata are almost deterministic in the sense that only one state has a non-deterministic choice when reading an input letter. In our model each state has a fixed probability to be final. We prove that for any d ≥ 1, with non-negligible probability the minimal (deterministic) automaton of the language recognized by such an automaton has more than n^d states; as a byproduct, the expected size of its minimal automaton grows faster than any polynomial. Our result also holds when each state is final with some probability that depends on n, as long as it is not too close to 0 and 1, at distance at least Ω(1/√n) to be precise, therefore allowing models with a sublinear number of final states in expectation.
Cite as

Arnaud Carayol, Philippe Duchon, Florent Koechlin, and Cyril Nicaud. One Drop of Non-Determinism in a Random Deterministic Automaton. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.STACS.2023.19,
  author =	{Carayol, Arnaud and Duchon, Philippe and Koechlin, Florent and Nicaud, Cyril},
  title =	{{One Drop of Non-Determinism in a Random Deterministic Automaton}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.19},
  URN =		{urn:nbn:de:0030-drops-176719},
  doi =		{10.4230/LIPIcs.STACS.2023.19},
  annote =	{Keywords: non-deterministic automaton, powerset construction, probabilistic analysis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2021.48
Absorbing Patterns in BST-Like Expression-Trees

Authors: Florent Koechlin and Pablo Rotondo

Published in: LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)

Abstract
In this article we study the effect of simple semantic reductions on random BST-like expression-trees. Such random unary-binary expression-trees are often used in benchmarks for model-checking tools. We consider the reduction induced by an absorbing pattern for some given operator ⊛, which we apply bottom-up, producing an equivalent (and smaller) tree-expression. Our main result concerns the expected size of a random tree, of given input size n → ∞, after reduction. We show that there are two different thresholds, leading to a total of five regimes, ranging from no significant reduction at all, to almost complete reduction. These regimes are completely characterized according to the probability of the absorbing operator. Our results prove that random BST-like trees have to be considered with care, and that they offer a richer range of behaviours than uniform random trees.
Cite as

Florent Koechlin and Pablo Rotondo. Absorbing Patterns in BST-Like Expression-Trees. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 48:1-48:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{koechlin_et_al:LIPIcs.STACS.2021.48,
  author =	{Koechlin, Florent and Rotondo, Pablo},
  title =	{{Absorbing Patterns in BST-Like Expression-Trees}},
  booktitle =	{38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
  pages =	{48:1--48:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-180-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{187},
  editor =	{Bl\"{a}ser, Markus and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.48},
  URN =		{urn:nbn:de:0030-drops-136933},
  doi =		{10.4230/LIPIcs.STACS.2021.48},
  annote =	{Keywords: BST trees, absorbing pattern, reduction, analytic combinatorics}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.114
Weakly-Unambiguous Parikh Automata and Their Link to Holonomic Series

Authors: Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud

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

Abstract
We investigate the connection between properties of formal languages and properties of their generating series, with a focus on the class of holonomic power series. We first prove a strong version of a conjecture by Castiglione and Massazza: weakly-unambiguous Parikh automata are equivalent to unambiguous two-way reversal bounded counter machines, and their multivariate generating series are holonomic. We then show that the converse is not true: we construct a language whose generating series is algebraic (thus holonomic), but which is inherently weakly-ambiguous as a Parikh automata language. Finally, we prove an effective decidability result for the inclusion problem for weakly-unambiguous Parikh automata, and provide an upper-bound on its complexity.
Cite as

Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-Unambiguous Parikh Automata and Their Link to Holonomic Series. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 114:1-114:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bostan_et_al:LIPIcs.ICALP.2020.114,
  author =	{Bostan, Alin and Carayol, Arnaud and Koechlin, Florent and Nicaud, Cyril},
  title =	{{Weakly-Unambiguous Parikh Automata and Their Link to Holonomic Series}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{114:1--114:16},
  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.114},
  URN =		{urn:nbn:de:0030-drops-125212},
  doi =		{10.4230/LIPIcs.ICALP.2020.114},
  annote =	{Keywords: generating series, holonomicity, ambiguity, reversal bounded counter machine, Parikh automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.47
Tree Automata with Global Constraints for Infinite Trees

Authors: Patrick Landwehr and Christof Löding

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
We study an extension of tree automata on infinite trees with global equality and disequality constraints. These constraints can enforce that all subtrees for which in the accepting run a state q is reached (at the root of that subtree) are identical, or that these trees differ from the subtrees at which a state q' is reached. We consider the closure properties of this model and its decision problems. While the emptiness problem for the general model remains open, we show the decidability of the emptiness problem for the case that the given automaton only uses equality constraints.
Cite as

Patrick Landwehr and Christof Löding. Tree Automata with Global Constraints for Infinite Trees. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 47:1-47:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{landwehr_et_al:LIPIcs.STACS.2019.47,
  author =	{Landwehr, Patrick and L\"{o}ding, Christof},
  title =	{{Tree Automata with Global Constraints for Infinite Trees}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{47:1--47:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.47},
  URN =		{urn:nbn:de:0030-drops-102863},
  doi =		{10.4230/LIPIcs.STACS.2019.47},
  annote =	{Keywords: Tree automata, infinite trees, global constraints}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.42
Optimal Strategies in Pushdown Reachability Games

Authors: Arnaud Carayol and Matthew Hague

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
An algorithm for computing optimal strategies in pushdown reachability games was given by Cachat. We show that the information tracked by this algorithm is too coarse and the strategies constructed are not necessarily optimal. We then show that the algorithm can be refined to recover optimality. Through a further non-trivial argument the refined algorithm can be run in 2EXPTIME by bounding the play-lengths tracked to those that are at most doubly exponential. This is optimal in the sense that there exists a game for which the optimal strategy requires a doubly exponential number of moves to reach a target configuration.
Cite as

Arnaud Carayol and Matthew Hague. Optimal Strategies in Pushdown Reachability Games. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.MFCS.2018.42,
  author =	{Carayol, Arnaud and Hague, Matthew},
  title =	{{Optimal Strategies in Pushdown Reachability Games}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{42:1--42:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul 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.MFCS.2018.42},
  URN =		{urn:nbn:de:0030-drops-96248},
  doi =		{10.4230/LIPIcs.MFCS.2018.42},
  annote =	{Keywords: Pushdown Systems, Reachability Games, Optimal Strategies, Formal Methods, Context Free}
}
  • Refine by Type
  • 17 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 7 2025
  • 1 2024
  • 1 2023
  • 1 2021
  • Show More...

  • Refine by Author
  • 6 Carayol, Arnaud
  • 3 Koechlin, Florent
  • 3 Nicaud, Cyril
  • 2 Niwiński, Damian
  • 2 Parys, Paweł
  • Show More...

  • Refine by Series/Journal
  • 17 LIPIcs

  • Refine by Classification
  • 6 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Logic and verification
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Regular languages
  • 2 Theory of computation → Tree languages
  • Show More...

  • Refine by Keyword
  • 2 lower bounds
  • 1 Automatic numbers
  • 1 BST trees
  • 1 Context Free
  • 1 Determinisation
  • 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