15 Search Results for "Casares, Antonio"

Document
DOI: 10.4230/LIPIcs.LICS.2026.21
Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches

Authors: Mikołaj Bojańczyk, Antonio Casares, Sven Manthe, and Paweł Parys

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

Abstract
Rabin’s Tree Theorem says that the {mso} theory of the infinite binary tree 2^* is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to 2^{≤ω}, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in 2^{≤ω} by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin’s Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.
Cite as

Mikołaj Bojańczyk, Antonio Casares, Sven Manthe, and Paweł Parys. Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.LICS.2026.21,
  author =	{Boja\'{n}czyk, Miko{\l}aj and Casares, Antonio and Manthe, Sven and Parys, Pawe{\l}},
  title =	{{Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{21:1--21: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.21},
  URN =		{urn:nbn:de:0030-drops-268080},
  doi =		{10.4230/LIPIcs.LICS.2026.21},
  annote =	{Keywords: MSO logic, automata over infinite trees, games on graphs}
}
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.29
Commutative Algebras of Series

Authors: Lorenzo Clemente

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

Abstract
We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A P-product of series is defined coinductively by a polynomial product rule P, which gives a recursive recipe to build the product of two series as a function of the series themselves and their derivatives. The first main result of the paper is a complete and decidable characterisation of all product rules P giving rise to P-products which are bilinear, associative, and commutative. The characterisation shows that there are infinitely many such products, and in particular it applies to the notable Hadamard, shuffle, and infiltration products from the literature. Every P-product gives rise to the class of P-automata, an infinite-state model where states are terms. The second main result of the paper is that the equivalence problem for P-automata is decidable for P-products satisfying our characterisation. This explains, subsumes, and extends previous results on Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.
Cite as

Lorenzo Clemente. Commutative Algebras of Series. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{clemente:LIPIcs.LICS.2026.29,
  author =	{Clemente, Lorenzo},
  title =	{{Commutative Algebras of Series}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{29:1--29:23},
  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.29},
  URN =		{urn:nbn:de:0030-drops-268167},
  doi =		{10.4230/LIPIcs.LICS.2026.29},
  annote =	{Keywords: formal power series, weighted automata, product rules, algebra, coalgebra}
}
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
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.149
The Memory of ω-Regular and BC(Σ⁰₂) Objectives

Authors: Antonio Casares and Pierre Ohlmann

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

Abstract
In the context of 2-player zero-sum infinite duration games played on (potentially infinite) graphs, the memory of an objective is the smallest integer k such that in any game won by Eve, she has a strategy with ≤ k states of memory. For ω-regular objectives, checking whether the memory equals a given number k was not known to be decidable. In this work, we focus on objectives in BC(Σ⁰₂), i.e. recognised by a potentially infinite deterministic parity automaton. We provide a class of automata that recognise objectives with memory ≤ k, leading to the following results: - for ω-regular objectives, the memory can be computed in NP; - given two objectives W₁ and W₂ in BC(Σ⁰₂) and assuming W₁ is prefix-independent, the memory of W₁ ∪ W₂ is at most the product of the memories of W₁ and W₂. Our results also apply to chromatic memory, the variant where strategies can update their memory state only depending on which colour is seen.
Cite as

Antonio Casares and Pierre Ohlmann. The Memory of ω-Regular and BC(Σ⁰₂) Objectives. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 149:1-149:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2025.149,
  author =	{Casares, Antonio and Ohlmann, Pierre},
  title =	{{The Memory of \omega-Regular and BC(\Sigma⁰₂) Objectives}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{149:1--149:18},
  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.149},
  URN =		{urn:nbn:de:0030-drops-235267},
  doi =		{10.4230/LIPIcs.ICALP.2025.149},
  annote =	{Keywords: Infinite duration games, Strategy complexity, Omega-regular}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.22
On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata

Authors: Antonio Casares, Olivier Idir, Denis Kuperberg, Corto Mascle, and Keya Prakash

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised Büchi automata is NP-complete, as well as the problem of minimising at the same time the number of states and colours of history-deterministic generalised coBüchi automata.
Cite as

Antonio Casares, Olivier Idir, Denis Kuperberg, Corto Mascle, and Keya Prakash. On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.CSL.2025.22,
  author =	{Casares, Antonio and Idir, Olivier and Kuperberg, Denis and Mascle, Corto and Prakash, Keya},
  title =	{{On the Minimisation of Deterministic and History-Deterministic Generalised (Co)B\"{u}chi Automata}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.22},
  URN =		{urn:nbn:de:0030-drops-227798},
  doi =		{10.4230/LIPIcs.CSL.2025.22},
  annote =	{Keywords: Automata minimisation, omega-regular languages, good-for-games automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.35
The Complexity of Simplifying ω-Automata Through the Alternating Cycle Decomposition

Authors: Antonio Casares and Corto Mascle

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller into parity automata and to obtain theoretical results about the possibility of relabelling automata with different acceptance conditions. In this work, we study the complexity of computing the ACD and its DAG-version, proving that this can be done in polynomial time for suitable representations of the acceptance condition of the Muller automaton. As corollaries, we obtain that we can decide typeness of Muller automata in polynomial time, as well as the parity index of the languages they recognise. Furthermore, we show that we can minimise in polynomial time the number of colours (resp. Rabin pairs) defining a Muller (resp. Rabin) acceptance condition, but that these problems become NP-complete when taking into account the structure of an automaton using such a condition.
Cite as

Antonio Casares and Corto Mascle. The Complexity of Simplifying ω-Automata Through the Alternating Cycle Decomposition. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.MFCS.2024.35,
  author =	{Casares, Antonio and Mascle, Corto},
  title =	{{The Complexity of Simplifying \omega-Automata Through the Alternating Cycle Decomposition}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.35},
  URN =		{urn:nbn:de:0030-drops-205916},
  doi =		{10.4230/LIPIcs.MFCS.2024.35},
  annote =	{Keywords: Omega-regular languages, Muller automata, Zielonka tree}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.54
Positionality in Σ⁰₂ and a Completeness Result

Authors: Pierre Ohlmann and Michał Skrzypczak

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in Σ⁰₂ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective W which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective W' which is equivalent to W over finite game graphs and positional over arbitrary game graphs.
Cite as

Pierre Ohlmann and Michał Skrzypczak. Positionality in Σ⁰₂ and a Completeness Result. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 54:1-54:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.STACS.2024.54,
  author =	{Ohlmann, Pierre and Skrzypczak, Micha{\l}},
  title =	{{Positionality in \Sigma⁰₂ and a Completeness Result}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{54:1--54:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.54},
  URN =		{urn:nbn:de:0030-drops-197643},
  doi =		{10.4230/LIPIcs.STACS.2024.54},
  annote =	{Keywords: infinite duration games, positionality, Borel class \Sigma⁰₂, history determinism}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.118
How to Play Optimally for Regular Objectives?

Authors: Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
Cite as

Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove. How to Play Optimally for Regular Objectives?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 118:1-118:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2023.118,
  author =	{Bouyer, Patricia and Fijalkow, Nathana\"{e}l and Randour, Mickael and Vandenhove, Pierre},
  title =	{{How to Play Optimally for Regular Objectives?}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{118:1--118:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.118},
  URN =		{urn:nbn:de:0030-drops-181700},
  doi =		{10.4230/LIPIcs.ICALP.2023.118},
  annote =	{Keywords: two-player games on graphs, strategy complexity, regular languages, finite-memory strategies, NP-completeness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.122
Characterising Memory in Infinite Games

Authors: Antonio Casares and Pierre Ohlmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper is concerned with games of infinite duration played over potentially infinite graphs. Recently, Ohlmann (TheoretiCS 2023) presented a characterisation of objectives admitting optimal positional strategies, by means of universal graphs: an objective is positional if and only if it admits well-ordered monotone universal graphs. We extend Ohlmann’s characterisation to encompass (finite or infinite) memory upper bounds. We prove that objectives admitting optimal strategies with ε-memory less than m (a memory that cannot be updated when reading an ε-edge) are exactly those which admit well-founded monotone universal graphs whose antichains have size bounded by m. We also give a characterisation of chromatic memory by means of appropriate universal structures. Our results apply to finite as well as infinite memory bounds (for instance, to objectives with finite but unbounded memory, or with countable memory strategies). We illustrate the applicability of our framework by carrying out a few case studies, we provide examples witnessing limitations of our approach, and we discuss general closure properties which follow from our results.
Cite as

Antonio Casares and Pierre Ohlmann. Characterising Memory in Infinite Games. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 122:1-122:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2023.122,
  author =	{Casares, Antonio and Ohlmann, Pierre},
  title =	{{Characterising Memory in Infinite Games}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{122:1--122:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.122},
  URN =		{urn:nbn:de:0030-drops-181740},
  doi =		{10.4230/LIPIcs.ICALP.2023.122},
  annote =	{Keywords: Infinite duration games, Memory, Universal graphs}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2022.3
The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk)

Authors: Patricia Bouyer, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Two-player turn-based zero-sum games on (finite or infinite) graphs are a central framework in theoretical computer science - notably as a tool for controller synthesis, but also due to their connection with logic and automata theory. A crucial challenge in the field is to understand how complex strategies need to be to play optimally, given a type of game and a winning objective. In this invited contribution, we give a tour of recent advances aiming to characterize games where finite-memory strategies suffice (i.e., using a limited amount of information about the past). We mostly focus on so-called chromatic memory, which is limited to using colors - the basic building blocks of objectives - seen along a play to update itself. Chromatic memory has the advantage of being usable in different game graphs, and the corresponding class of strategies turns out to be of great interest to both the practical and the theoretical sides.
Cite as

Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs (Invited Talk). In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2022.3,
  author =	{Bouyer, Patricia and Randour, Mickael and Vandenhove, Pierre},
  title =	{{The True Colors of Memory: A Tour of Chromatic-Memory Strategies in Zero-Sum Games on Graphs}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.3},
  URN =		{urn:nbn:de:0030-drops-173957},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.3},
  annote =	{Keywords: two-player games on graphs, finite-memory strategies, chromatic memory, parity automata, \omega-regularity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.20
Half-Positional Objectives Recognized by Deterministic Büchi Automata

Authors: Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
A central question in the theory of two-player games over graphs is to understand which objectives are half-positional, that is, which are the objectives for which the protagonist does not need memory to implement winning strategies. Objectives for which both players do not need memory have already been characterized (both in finite and infinite graphs); however, less is known about half-positional objectives. In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, in both finite and infinite graphs. Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
Cite as

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2022.20,
  author =	{Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Half-Positional Objectives Recognized by Deterministic B\"{u}chi Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.20},
  URN =		{urn:nbn:de:0030-drops-170833},
  doi =		{10.4230/LIPIcs.CONCUR.2022.20},
  annote =	{Keywords: two-player games on graphs, half-positionality, memoryless optimal strategies, B\"{u}chi automata, \omega-regularity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.117
On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games

Authors: Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen

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

Abstract
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.
Cite as

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
DOI: 10.4230/LIPIcs.CSL.2022.12
On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions

Authors: Antonio Casares

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
In this paper, we relate the problem of determining the chromatic memory requirements of Muller conditions with the minimisation of transition-based Rabin automata. Our first contribution is a proof of the NP-completeness of the minimisation of transition-based Rabin automata. Our second contribution concerns the memory requirements of games over graphs using Muller conditions. A memory structure is a finite state machine that implements a strategy and is updated after reading the edges of the game; the special case of chromatic memories being those structures whose update function only consider the colours of the edges. We prove that the minimal amount of chromatic memory required in games using a given Muller condition is exactly the size of a minimal Rabin automaton recognising this condition. Combining these two results, we deduce that finding the chromatic memory requirements of a Muller condition is NP-complete. This characterisation also allows us to prove that chromatic memories cannot be optimal in general, disproving a conjecture by Kopczyński.
Cite as

Antonio Casares. On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{casares:LIPIcs.CSL.2022.12,
  author =	{Casares, Antonio},
  title =	{{On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.12},
  URN =		{urn:nbn:de:0030-drops-157322},
  doi =		{10.4230/LIPIcs.CSL.2022.12},
  annote =	{Keywords: Automata on Infinite Words, Games on Graphs, Arena-Independent Memory, Complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.123
Optimal Transformations of Games and Automata Using Muller Conditions

Authors: Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow

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

Abstract
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.
Cite as

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}
}
  • Refine by Type
  • 15 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 3 2025
  • 2 2024
  • 2 2023
  • 4 2022
  • Show More...

  • Refine by Author
  • 10 Casares, Antonio
  • 3 Bouyer, Patricia
  • 3 Ohlmann, Pierre
  • 3 Randour, Mickael
  • 3 Vandenhove, Pierre
  • Show More...

  • Refine by Series/Journal
  • 15 LIPIcs

  • Refine by Classification
  • 5 Theory of computation → Automata over infinite objects
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Verification by model checking
  • 1 Theory of computation → Algorithmic game theory
  • Show More...

  • Refine by Keyword
  • 3 Infinite duration games
  • 3 two-player games on graphs
  • 2 Muller games
  • 2 finite-memory strategies
  • 2 good-for-games automata
  • 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