We study 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, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.

翻译：我们研究了参与者数量无界且与不可控环境交互的分布式系统的反应式合成问题。这些系统的执行过程通过数据词建模，规约由一种称为前缀一阶逻辑的片段给出，该逻辑实现了一种有限阶序关系。我们证明该逻辑具有良好的性质，能够使我们证明合成问题的可判定性。