Church Synthesis on Register Automata over Linearly Ordered Data Domains (STACS 2021)


Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data $\omega$‑words. We study the synthesis problem for specifications given as register automata over a linearly ordered data domain (e.g. $(\mathbb{N}, \leq)$ or $(\mathbb{Q}, \leq)$), which allow for comparison of data with regards to the linear order. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately play some data, and Eve wins whenever their interaction complies with the specification, which is a language of $\omega$‑words over ordered data. Such games are however undecidable, even when the specification is recognised by a deterministic register automaton. This is in contrast with the equality case, where the problem is only undecidable for nondeterministic and universal specifications.

Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and deciding the existence of a winning strategy is in ExpTime, both for $\mathbb{Q}$ and $\mathbb{N}$. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to $\omega$‑regular games. Lastly, we apply these results to the transducer synthesis problem for input-driven register automata, where each output data is restricted to be the content of some register, and show that if there exists an implementation, then there exists one which is a register transducer.

38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany

While generalising our results about register-bounded and unbounded synthesis over $(\mathbb{N},=)$ (presented here) to the case of $(\mathbb{Q},<)$ is relatively straightforward, the case of $(\mathbb{N},<)$ is significantly more difficult, as behaviours of register automata over the latter domain cannot be abstracted in an $\omega$‑regular way. In this paper, we however show that they can be regularly approximated. This contribution is detailed in Chapter 7 of my manuscript (more precisely Section 7.3.4), which also features a simpler proof of the key lemma (Lemma 16 in the paper, 7.25 in the manuscript).

Ayrat presented this work at STACS 2021. He also gave a more in-depth talk about it at the IRIF “Automates” seminar. The link is not public, but you might consider contacting the organisers of the seminar to ask for it.