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.

History-deterministic Register Automata @ NWPT 2021

History-deterministic register automata form a promising class for synthesis and runtime verification applications.

Automatic Synthesis of Systems with Data

We partly lift synthesis to infinite domains through register automata, targeting register transducers or computable implementations.

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.

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.

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.

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.

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.

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.

On Computability of Data Word Functions Defined by Transducers

We extend the correspondence between computability and continuity over regular functions to the case of data words.