Synthesis over Infinite Domains through Machines with Registers @ Journées GT Vérif 2021 (Invited talk)

Abstract

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 ($\omega$‑words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite.

The aim of this talk is to investigate the case of infinite alphabets. Correspondingly, executions are modelled as data $\omega$‑words. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers, used to store and compare data values. We consider different instances, depending on whether the specification is nondeterministic, universal (a.k.a. co-nondeterministic) or deterministic: contrary to the finite-alphabet case, those classes are expressively distinct.

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 $\omega$‑regular way. A further exploration of the problem allows to extend the results to the discrete order $(\mathbb{N},<)$, where the behaviours can be regularly approximated. Finally, decidability can be transferred to the case of words with the prefix relation $(\mathbb{\Sigma}^*,\prec)$ through a notion of reducibility between domains.