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 (
In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.
We have been invited to write an extended version of this paper, that appeared in the LMCS special issue dedicated to CONCUR 2019. It contains full proofs and provides a simplified proof for the unbounded case; see this page for more details. The proofs have been further distilled in Chapters 5-8 of my manuscript.