In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (
The aim of this talk is to investigate the case of infinite alphabets. Correspondingly, executions are modelled as data
When the number of registers of the target implementation is unbounded, the synthesis problem is undecidable, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but decidability is recovered for universal ones.
The study was initially conducted over data domains with the equality predicate only, but the techniques can be lifted to the dense order $(\mathbb{Q},<)$ and so-called oligomorphic data domains, over which register automata behave in an
I have been invited to give a talk at the Journées du GT Vérif, that will take place at ENS Paris Saclay (Gif-sur-Yvette, France) from the 17th to the 19th of November 2021. I will be in Paris for the week, do not hesitate to contact me if you want to meet at this occasion. The event simultaneously happens online, so you can also follow the talk via Zoom.