En | Fr | Es

Antonio Casares Santos

I am a postdoctoral researcher in Theoretical Computer Science at the RPTU, University of Kaiserslautern-Landau (Germany), working in the group of Anthony Lin.

My research interests lie in the intersection of logic, formal languages and games on graphs. More specifically, my research focuses on ω-automata, algorithms for solving infinite duration games and finite model theory.

Before coming to Kaiserslautern, I was a postdoc at the University of Warsaw (Poland) with Mikołaj Bojańczyk. I received my doctoral degree in 2023 from the University of Bordeaux, under the supervision of Nathanaël Fijalkow and Igor Walukiewicz. Before that, I obtained my master's degree in Mathematical Logic and Foundations of Computer Science at Université de Paris-Cité (France).

You will find more information in my CV.

Links:

I gathered some links with advice about different aspects of academic life here.

I support:

Research

A full list of my publications can also be found in my dblp and Google Scholar sites.

PhD Thesis

Structural properties of automata over infinite words and memory for games, 2023, Université de Bordeaux - Manuscript of the thesis (pdf) - Bibtex - Slides

My thesis has been awarded the "Science and technology" prize from the University of Bordeaux! (link)

Book chapters

Chapter Positionality and Memory in the book Games on Graphs: From Logic and Automata to Algorithms (coauthored by Pierre Ohlmann and Pierre Vandenhove) - arxiv link - bibtex of chapter.

Surveys

Transition-based vs stated-based acceptance for automata over infinite words. In: Bulletin EATCS, Oct 2025 - pdf.

Publications in peer-reviewed journals and conference proceedings

The memory of ω-regular and BC(Σ₂) objectives (with Pierre Ohlmann). In: ICALP 2025 - conf version - full version - bibtex.
Positional ω-regular languages (with Pierre Ohlmann). In: LICS 2024 & TheoretiCS (2026) - conf version - journal version - bibtex.
Fast value iteration: A uniform approach to efficient algorithms for energy games (with Michaël Cadilhac and Pierre Ohlmann). In: TACAS 2025 - pdf.
From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History) Determinism (with Thomas Colcombet, Nathanaël Fijalkow and Karoliina Lehtinen). In: TheoretiCS (2024) - pdf - bibtex.
On the Minimisation of Deterministic and History-Deterministic Generalised (co)Büchi Automata (with Olivier Idir, Denis Kuperberg, Corto Mascle and Aditya Prakash). In: CSL 2025 - pdf.
The Complexity of Simplifying ω-Automata through the Alternating Cycle Decomposition (with Corto Mascle). In: MFCS 2024 - short version - full version- bibtex.
Simple and Tight Complexity Lower Bounds for Solving Rabin Games (with Marcin Pilipczuk, Michał Pilipczuk, Uéverton S. Souza, K. S. Thejaswini). In: SOSA 2024 - pdf - bibtex.
Characterising Memory in Infinite Games (with Pierre Ohlmann). In: ICALP 2023 & LMCS (2025) - journal version - conf version - bibtex.
Half-Positional Objectives Recognized by Deterministic Büchi Automata (with Patricia Bouyer, Mickael Randour and Pierre Vandenhove). In: CONCUR 2022 & IJCAI 2023 & LMCS (2024) - journal version - conf version - extended abstract - bibtex.
On the Size of Good-For-Games Rabin Automata and Its Link with the Memory in Muller Games (with Thomas Colcombet and Karoliina Lehtinen). In: ICALP 2022 - pdf - bibtex.
Practical Applications of the Alternating Cycle Decomposition (with Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin and Salomon Sickert). In: TACAS 2022 - full version - bibtex.
On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions. In: CSL 2022 - short version - full version - bibtex. Best Student Paper Award.
Optimal Transformations of Games and Automata using Muller Conditions (with Thomas Colcombet and Nathanaël Fijalkow). In: ICALP 2021 - conf version - journal version - bibtex.

Preprints and submissions

Layered automata: A canonical model for automata over inﬁnite words (with Christof Löding and Igor Walukiewicz). Submitted to: LICS 2026 - pdf.
History-Deterministic Büchi Automata are Succinct (with Aditya Prakash and K.S Thejaswini). Submitted to: LICS 2026 - pdf.
Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches (with Mikołaj Bojańczyk, Sven Manthe and Paweł Parys). Submitted to: LICS 2026.
Infinite lexicographic products of positional objectives (with Pierre Ohlmann, Michał Skrzypczak and Igor Walukiewicz). Submitted to: LMCS - pdf.
A positional Π₃⁰-complete objective (with Pierre Ohlmann and Pierre Vandenhove), 2024 - pdf - bibtex.

Talks

Some slides and other resources

An Automata Model for Borel-MSO - pdf - animations.
Layered Automata: A Canonical Model for ω-Regular Languages - long pdf - short animated.
How to write a good introduction - slides.
Fast Value Iteration: A Uniform Framework for Energy Games - slides.
Safety and Liveness. Some thoughts - slides.
Canonical Models of Automata - slides.
State-Based vs Transition-Based Acceptance in ω-Automata - slides.
The Memory of ω-Regular Languages - short version - long version.
Positional ω-Regular Languages - old slides - poster.
Simplifying ω-Automata through the Alternating Cycle Decomposition - slides.
Minimisation of (History) Deterministic Generalised (co)Büchi Automata - slides.
Half-Positional Objectives Recognized by Deterministic Büchi Automata - slides.
On a Correspondence Between Memory Structures for Muller Games and Rabin Automata.- slides.
Good-For-Games Rabin Automata and the Memory Requirements of Muller Conditions.- slides- poster.
Minimisation of Transition-Based Rabin Automata - slides - poster.
Optimal Transformations of Games and Automata using Muller Conditions - slides.
Open Problem: Memory Requirements for Generalised Reachability games - poster.
Can we program without while loops? - slides - old slides in Spanish - video youtube.

Students

Current students

Émilie Neyraud (ENS Lyon). M2 internship on: Algorithmic aspects of layered automata.

Past students

Kacper Lewandowski (University of Warsaw, 2025). Master thesis on: History-deterministic coBüchi automata.
Alan Le Brech (ENS Rennes, 2025). M1 internship on: Universal value-iteration algorithms for games on graphs.

Teaching

2026, Summer semester (RPTU, University Kaiserslautern-Landau)

Automated Reasoning (Master course. Lectures on CDCL, Presburger and real arithmetic, the simplex method).

2023 - 2024 (University of Warsaw)

Algorithmic Aspects of Game Theory (Tutorials and some lectures).

Contact

E-mail
antonio.casares [at] rptu [dot] de

Location
Building 34, Office 428 RPTU, Gottlieb-Daimler-Straße 67663 Kaiserslautern (Germany)