Register Automata

Synthesis over Infinite Domains through Machines with Registers @ Journées GT Vérif 2021 (Invited talk)
Synthesis can be lifted to infinite domains through register automata, targeting register transducers implementations.
Léo Exibard
Nov 18, 2021
PDF Details
History-deterministic Register Automata @ NWPT 2021
History-deterministic register automata form a promising class for synthesis and runtime verification applications.
Léo Exibard, Karoliina Lehtinen
Nov 5, 2021
PDF Slides Video
Automatic Synthesis of Systems with Data
We lift synthesis to infinite domains through register automata, targeting register transducers or computable implementations.
Léo Exibard
Sep 20, 2021
Manuscript Slides Video
On Computability of Data Word Functions Defined by Transducers @ ETAPS 2021
We extend the correspondence between computability and continuity over regular functions to the case of data words.
Léo Exibard
Apr 1, 2021
PDF Slides Details
Church Synthesis on Register Automata over Linearly Ordered Data Domains (STACS 2021)
The Church game for register automata over $(\mathbb{N}, \leq)$ is undecidable, but the one-sided game is, for deterministic ones.
Léo Exibard, Emmanuel Filiot, Ayrat Khalimov
PDF Cite DOI
On Computability of Data Word Functions Defined by Transducers @ HIGHLIGHTS 2020
We extend the correspondence between computability and continuity over regular functions to the case of data words.
Léo Exibard
Sep 17, 2020
PDF Poster Slides Video Details
On Computability of Data Word Functions Defined by Transducers @ MOVEP 2020
We extend the correspondence between computability and continuity over regular functions to the case of data words.
Léo Exibard
Jun 25, 2020
PDF Slides Video Details
Synthesis of Data Word Transducers (LMCS Special Issue dedicated to CONCUR 2019)
Register automata are a counterpart of finite automata over data words. Synthesis algorithms can (sometimes) be extended to them.
Léo Exibard, Emmanuel Filiot, Pierre-Alain Reynier
PDF Cite Poster Slides DOI Conference
On Computability of Data Word Functions Defined by Transducers (FoSSaCS 2020)
We extend the correspondence between computability and continuity over regular functions to the case of data words.
Léo Exibard, Emmanuel Filiot, Pierre-Alain Reynier
PDF Cite Poster Slides Video DOI Journal Short video
Synthesis of Data Word Transducers (CONCUR 2019)
Register automata are a counterpart of finite automata over data words. Synthesis algorithms can (sometimes) be extended to them.
Léo Exibard, Emmanuel Filiot, Pierre-Alain Reynier
PDF Cite Poster Slides DOI Journal