Denis Kuperberg

I am a CNRS researcher at LIP, ENS Lyon, Plume team.

Some research interests: automata theory, synthesis, verification, games, logics, decidability procedures, complexity, proof theory, interdisciplinary research.

Email: denis.kuperberg [at] ens-lyon.fr

Curriculum Vitae: in English, in French

I support :

Research

Supervision

Present

Thomas Kosc: Postdoctorate, with Sylvain Charlat and Etienne Rajon

Past

Quentin Moreau: L3 internship
Hugo Francon: M2 internship, with Nathanaël Fijalkow
Olivier Idir: PLR (pre-doc)
Émile Hazard : PhD
Fatemeh Ghasemi : M1 internship, with Amina Doumane
Laureline Pinault : PhD, with Damien Pous
Alixel Bagnis : L3 internship
Milla Valnet : L3 internship
Jan Martens : M2 internship
Marc Bagnol : Postdoctorate
Anirban Majumdar : M1 internship

Preprints:

Explorable Parity Automata
With Émile Hazard, Olivier Idir.
Extended version of the CSL 2023 paper.

Thermodynamic consistency of autocatalytic cycles
With Thomas Kosc, Etienne Rajon, Sylvain Charlat.

Tree algebras and bisimulation-invariant MSO on finite graphs
With Thomas Colcombet and Amina Doumane.

Positive and monotone fragments of FO and LTL
With Quentin Moreau.

On the Minimisation of Deterministic and History-Deterministic Generalised (co)Büchi Automata
With Antonio Casares, Olivier Idir, Corto Mascle, Aditya Prakash.
Accepted for publication in CSL 2025.

(Recent) Publications:

A list of my publications is also available on DBLP.
Or see here for a complete list of publications and talks.

Positive First-order Logic on Words and Graphs
In LMCS 2023.
Here is the conference version, distinguished paper at LICS 2021.

Explorable Automata
With Émile Hazard, in CSL 2023.

Bouncing threads for infinitary and circular proofs
With David Baelde, Amina Doumane and Alexis Saurin, in LICS 2022.

Cyclic Proofs for Transfinite Expressions
With Émile Hazard, in CSL 2022.

Cyclic Proofs, System T, and the Power of Contraction
with Laureline Pinault and Damien Pous, in POPL 2021.

On the Succinctness of Alternating Parity Good-for-Games Automata
with Udi Boker, Karoliina Lehtinen and Michał Skrzypczak, in FSTTCS 2020.

Regular Resynchronizability of Origin Transducers is Undecidable
with Jan Martens, in MFCS 2020.

Cyclic Proofs and Jumping Automata
with Laureline Pinault and Damien Pous, in FSTTCS 2019.

Eventually Safe Languages
with Simon Iosti, in DLT 2019.

Coinductive algorithms for Büchi automata
with Laureline Pinault and Damien Pous, in Fundamenta Informaticae, special issue of DLT 2019.
Conference version here.

Kleene Algebra with Hypotheses
with Amina Doumane, Damien Pous and Cécilia Pradic, in FoSSaCS 2019.

Sensing as a Complexity Measure
Survey paper on sensing,
With Shaull Almagor and Orna Kupferman, in IJFCS 2019.
Conference version in DFCS 2017.

Computing the Width of Non-deterministic Automata
With Anirban Majumdar, in LMCS 2019.
Conference Version: Width of Non-deterministic Automata in STACS 2018 .

Büchi Good-for-Games Automata are Efficiently Recognizable
with Marc Bagnol, in FSTTCS 2018.

Soundness in Negotiations
With Javier Esparza, Anca Muscholl and Igor Walukiewicz, in LMCS 2018.
Conference version in CONCUR 2016.

Stamina: Stabilisation Monoids IN Automata theory
Presenting the tool Stamina,
with Nathanaël Fijalkow, Hugo Gimbert and Edon Kelmendi, in CIAA 2017.

On Finite Domains in First-Order Linear Temporal Logic
With Julien Brunel and David Chemouil, in ATVA 2016.

Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations
Presenting the tool Electrum,
with Nuno Macedo, Julien Brunel, David Chemouil and Alcino Cunha, in FSE 2016.

Varieties of Cost Functions
With Laure Daviaud and Jean-Éric Pin, in STACS 2016.

Cost Functions Definable by Min/Max Automata
With Thomas Colcombet, Amaldev Manuel and Szymon Toruńczyk, in STACS 2016.

The Sensing Cost of Monitoring and Synthesis
With Shaull Almagor and Orna Kupferman, in FSTTCS 2015.

On Determinisation of Good-for-Games Automata
With Michał Skrzypczak, in ICALP 2015.

Trading Bounds for Memory in Games with Counters
With Nathanaël Fijalkow, Florian Horn and Michał Skrzypczak, in ICALP 2015.

Regular Sensing.
With Saull Almagor and Orna Kupferman, in FSTTCS 2014.

ACME: Automata with Counters, Monoids and Equivalence.
Presenting the tool Acme,
With Nathanaël Fijalkow, in ATVA 2014.

Two-Way Cost Automata and Cost Logics over Infinite Trees.
With Achim Blumensath, Thomas Colcombet, Paweł Parys and Michael Vanden Boom, in CSL-LICS 2014.

Linear Temporal Logic for Regular Cost Functions.
in LMCS 2014.
This work contains an error: ERRATUM.
Conference version in STACS 2011.

Deciding the weak definability of Büchi definable tree languages.
With Thomas Colcombet, Christof Löding, and Michael Vanden Boom, in CSL 2013.

Nondeterminism in the Presence of a Diverse or Unknown Future.
With Udi Boker, Orna Kupferman, and Michał Skrzypczak, in ICALP 2013.

On the Expressive Power of Cost Logics over Infinite Words.
With Michael Vanden Boom, in ICALP 2012.

Quasi-Weak Cost Automata: A New Variant of Weakness.
With Michael Vanden Boom, in FSTTCS 2011.

Regular Temporal Cost Functions.
With Thomas Colcombet and Sylvain Lombardy, in ICALP 2010.

Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation.
With Peter Dybjer, in Annals of Pure and Applied Logic, 2012.

To see and download older papers, click on

Software

EmergeNS: In development, a software generating and simulating networks of chemical reactions, and tracking autocatalytic dynamics in them.
Programmed in C++, using the frameworks JUCE and JUCE Organic UI, and the SMT Solver Z3.
This is part of an interdisciplinary project with Sylvain Charlat, Thomas Kosc, Etienne Rajon.

Stamina : Implements algebraic techniques to solve decision problems from automata theory and cost function theory, including the star-height problem. Improvement on ACME, with optimizations and more functionalities. It solves the following problems:
- Star-height for regular languages,
- Boundedness for cost automata,
- Value 1 for probabilistic automata (not in full generality because it is undecidable).
Programmed in C++, with Nathanael Fijalkow, Hugo Gimbert and Edon Kelmendi.

Electrum : Consists of
- A formal specification language mixing relational first-order logic (RFOL) and linear temporal logic (LTL),
- An Analyzer for Electrum models, producing SMV files that can be processed with nuXmv.
Programmed in OCaml, with Julien Brunel and David Chemouil.

Acme : Implements algebraic techniques to solve decision problems from automata theory and cost function theory. The core generic algorithm takes as input an automaton and computes its stabilization monoid, which is a generalization of its transition monoid.
Programmed in OCaml, with Nathanael Fijalkow.

Thesis:

My thesis is entitled "Study of classes of regular cost functions", and explores a new quantitative extension of the theory of regular languages.
Here is my PHD manuscript (in french).

If the thesis is too long or if you don't speak french, here is a short summary (20 pages) in english, and the slides of the defense, also in english.

Talks

Click on the titles for slides.

20/09/24: Explorable Automata at Highlights of Logic, Games and Automata 2024, Bordeaux.
13/06/24: Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs at MOVE Team Seminar, Marseille.
14/05/24: History-deterministic and Explorable automata at GREYC Seminar, Caen.
26/04/24: Explorable automata at GT DAAL, Rennes.
24/04/24: Positive and monotone fragments of FO and LTL at ATLAS workshop, Rennes.
11/12/23: SMT Solving and modeling for biology at Plume team seminar, Lyon.
24/11/23: Positive First-Order Logic on Words and Graphs at Birmingham Theory Seminar.
26/07/23: Positive First-Order Logic on Words and Graphs at Highlights of Logic, Games and Automata, Kassel.
28/06/23: Computational content of circular proof systems at Lambda Pros day, Paris.
16/02/23: Explorable Automata at CSL 2023, Warsaw.
30/05/22: Explorable Automata at Delta ANR Meeting, CIRM, Marseille.
10/03/22: Positive first-order logic on words and graphs at Chocola Meeting, ENS Lyon.
04/01/22: Positive first-order logic on words at Delta ANR Meeting, online.
09/11/21: Good-for-Games Automata: State of the art and perspectives at Workshop on Unambiguity in Automata Theory, Dagstuhl.
03/11/21: Positive first-order logic on words at Warwick Seminar, online.
28/09/21: Positive first-order logic on words at LaBRI Seminar, Bordeaux.
16/09/21: Positive first-order logic on words at Highlights 2021, online.
30/04/21: Positive first-order logic on words at IRIF Automata Seminar, online.
16/12/20: Positive first-order logic on words (blackboard talk) at Warsaw automata seminar, online.
06/11/20: Recognizing Good-for-Games Automata: the G2 conjecture at IRIF Automata Seminar, online.
16/09/20: Positive first-order logic on words at Highlights 2020, online, also with Poster Session.
13/05/20: Computational content of circular proof systems at Warsaw Automata Seminar, online.
21/01/20: Computational content of circular proof systems at Formal Method Seminar, Labri, Bordeaux.

07/11/19: Cyclic Proofs and Jumping Automata at MoVe Seminar, LIS, Marseille.

20/09/19: Cyclic Proofs and Jumping Automata at Highlights of Logics, Games and Automata, Warsaw.

11/04/19: Kleene algebra with hypotheses at FoSSaCS, ETAPS, Prague.

07/04/19: Bouncing threads for infinitary and circular proofs at Galop Workshop, ETAPS, Prague.

11/02/19: Bouncing threads for infinitary and circular proofs (blackboard talk) at GdT PLume, Lyon.

30/10/18: Is your automaton good for playing games ? at DIMAP seminar, University of Warwick.

19/09/18: Is your automaton good for playing games ? at Highlights of Logic, Games and Automata, Berlin.

04/07/18: Parity Games and Good-for-Games Automata at Journées SDA2, Saint-Étienne.

13/04/18: Good-for-games automata and Width of Non-deterministic Automata (blackboard talk) at Automata Seminar, IRIF, Paris.

28/06/17: Stamina: Stabilisation Monoids in Automata theory at CIAA 2017, Marne-la-Vallée. Also with Tool demo.

01/02/17: Good-for-Games Automata at University of Oxford.

12/01/17: Soundness in Negotiations at Séminaire 68NQRT, IRISA, Rennes.

08/09/16: Soundness in Negotiations at Highlights of Automata, Bruxelles.

22/08/16: Soundness in Negotiations at Automata, Logic and Games, Singapore.

24/06/16: Directed Minors for Minimal Automata (blackboard talk) at Workshop Topology and Languages, IMT, Toulouse.

12/04/16: Good-for-Games Automata at GT-ALGA, Marseille.

25/02/16: Sensing Cost for Automata and Synthesis at MOVE Seminar, LIF, Marseille.

18/02/16: Varieties of Cost Functions at STACS 2016, Orléans.

18/02/16: Cost Functions Definable by Min/Max Automata at STACS 2016, Orléans.

16/02/16: Sensing Cost for Automata and Synthesis at Formal Method Seminar, Labri, Bordeaux.

24/11/15: Minimizing the sensing cost in monitoring and synthesis at IAS Kick-off Meeting, Munich.

19/11/15: Good-for-Games Automata versus Deterministic Automata at Plume Team Seminar, LIP, Lyon.

04/07/15: On Finite Domains in First-Order Linear Temporal Logic at LCC Workshop, Kyoto.

11/05/15: Theoretical Results around Electrum at Onera, DTIM Seminar, Toulouse.

22/04/15: On Finite Domains in First-Order Linear Temporal Logic at FAC days, Toulouse.

22/04/15: Regular Sensing at FAC days, Toulouse.

12/02/15: Good-for-Games Automata versus Deterministic Automata at LIF seminar, MoVe team, Marseille.

05/01/15: Good-for-Games Automata versus Deterministic Automata at LACL seminar, Créteil.

18/12/14: Cost Functions and Value 1 problem in practice at LABRI, Bordeaux, Séminaire Modélisation et Vérification.

06/10/14: Decidability problems in Automata theory at Onera, DTIM Seminar, Toulouse.

05/09/14: Regular Sensing at Highlights of Games, Logics and Automata, Paris.

07/07/14: On Determinisation of History-Deterministic Automata at YR-ICALP, Copenhagen. Also with Poster session.

22/05/14: Regular cost functions: from finite words to infinite trees at ENS Lyon, Plume Seminar.

30/04/14: Quasi-weak cost functions at the FREC meeting, CIRM, Marseille.

29/01/14: Regular Sensing (blackboard talk) at the Automata Seminar of Warsaw University, Poland.

07/01/14: Nondeterminism in the Presence of Diverse or Unknown Future at the Graph and Logics seminar, LABRI, Bordeaux.

04/12/13: Nondeterminism in the Presence of Diverse or Unknown Future (blackboard talk) at the Automata Seminar of Warsaw University, Poland.

15/05/13: The theory of regular cost functions (blackboard talk) at the Automata Seminar of Warsaw University, Poland.

10/05/13: The theory of regular cost functions at Quantitative Formal Methods Workshop, Jerusalem, Israel

01/05/13: The theory of regular cost functions at the Logic Seminar of Tel-Aviv University, Israel

19/03/13: Regular cost functions, from finite words to infinite trees at LSV seminar, ENS Cachan

05/03/13: Regular cost functions, from finite words to infinite trees at seminar 68NQRT, IRISA/INRIA Rennes

03/12/12: PhD Defense in LIAFA, Paris

23/10/12: La théorie des fonctions de coût régulières, at the Graph and Logics seminar, LABRI, Bordeaux

24/02/12: Expressive Power of Cost Logics over Infinite Words, at the Automata Seminar, LIAFA, Paris

12/12/11: Quasi-weak cost automata: a new variant of weakness at FSTCCS 2011, Mumbai, India

10/05/11: How to count with LTL, at the FREC ANR meeting, Ile de Ré

12/03/11: Linear Temporal Logic for regular cost functions at STACS 2011, Dortmund, Germany

23/02/11: Linear Temporal Logic for Regular Cost Functions, at the PhD Students Seminar, Liafa, Paris

10/07/10: Regular temporal cost functions at ICALP 2010, Bordeaux

17/11/09: The timed fragment of regular cost functions, at Workshop on Distance Automata and Generalisations, Liafa, Paris.

06/11/09: Regular cost functions, à la journée de rentrée du Liafa, Paris.

Teaching

Fall Semester 2021

ENS Lyon Master 2 course with Valeria Vignudelli: Mathematical Aspects of Automata Theory

Fall Semester 2020

ENS Lyon Master 2 course with Matteo Mio and Valeria Vignudelli: Mathematical Aspects of Automata Theory

Fall Semester 2018

ENS Lyon Master 2 course with Matteo Mio: Logic, Automata and Games for Advanced Verification

Spring Semester 2018

ENS Lyon Master 1 course: Semantics and Verification

Fall Semester 2017

ENS Lyon Master 2 course with Matteo Mio: Monadic Second Order Logic, Automata, Expressivity and Decidability

Fall Semester 2016

ENS Lyon Master 2 course with Colin Riba and Matteo Mio: Monadic Second Order Logic, Automata, Expressivity and Decidability

Popularisation

Here are slides of talks I have given for popularisation of mathematics, most of them in french:

Histoire des maths pour un "apéro curieux" informel.
NP-complétude: de la théorie à la pratique pour Open Minds 2023 à l'ENS Lyon.
Intelligence Artificielle: Midjourney, ChatGPT et autres pour un "apéro curieux" informel.
Chercheur en maths: le goût du jeu pour le forum des métiers du collège Honoré de Balzac de Vénissieux.
Les mathématiques du jonglage, pour la Maison des Maths et de l'Informatique (MMI) de Lyon.
Les paradoxes en mathématiques, pour les gagnants du concours de cryptographie Alkindi (niveau 3e et 2nde) en visite à l'ENS Lyon.
Les algorithmes d'apprentissage, sur Turing et l'histoire des algorithmes d'échecs et de go. Festival Pint of Science 2019 à Lyon.
Les algorithmes d'apprentissage, sur Turing et l'histoire des algorithmes d'échecs et de go. Fête de la Science 2018 in Lyon.
Les algorithmes d'apprentissage, sur l'histoire des algorithmes jouant aux échecs et au go, culminant avec Alphazero. Festival Pint of Science 2018 à Lyon.
IA et Robotique, sur l'intelligence artificielle et la robotique, donné en décembre 2017 lors d'un évènement organisé pour des agents d'entretien (en formation ou en activité). En association avec Plaisir Maths.
Des problèmes impossibles à l'intelligence artificielle, version étendue de PoS 2017 ci-dessous. École d'été SummerIA 2017.
Repousser les limites de l'informatique, sur les liens entre la notion de hasard et l'intelligence artificielle. Festival Pint of Science 2017 à Lyon.
Le Tsunami AlphaGo: une brève histoire de l'intelligence artificielle, jusqu'à l'arrivée d'Alphago. En partenariat avec Plaisir Maths.
Comment les mathématiciens ont inventé l'ordinateur, sur l'histoire de l'informatique.
The Mathematics of Juggling, for the polish journal Delta.
Théorème de Gödel pour le journal Prisme à idées.

Links

Mathematics

CS Theory Stackexchange
Free SF Stories by Greg Egan
Delightful Puzzles
Images des Mathématiques
The Beauty of roots: An unexpected escapade
A Mathematician's lament: On education in mathematics
Science etonnante: A good science blog, in french

Hobbies

Home Research Talks Teaching Links

Research

Teaching

Links

Home

Research

Talks

Teaching

Links