Synthesis for fragments of first-order logic on data words

We carry on the study initiated by Bérard et al.[1] of the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words (i.e. finite or infinite words were positions are labeled by an unbounded alphabet), and specifications are given as first-order formulas.

First, we delineate the border between decidability and undecidability for the fragments introduced by Bérard et al.[1]. We then introduce prefix first-order logic, a logic that implements a limited kind of order, and show that this logic has a decidable synthesis problem on data words.

[1] Bérard Béatrice, et al. “Parameterized Synthesis for Fragments of First-Order Logic Over Data Words.” FoSSaCS. 2020.