Synthesis for prefix first-order logic on data words

TL;DR

This paper investigates the reactive synthesis problem for distributed systems modeled by data words, using a specific fragment of first-order logic called prefix first-order logic, and proves its decidability.

Contribution

It introduces prefix first-order logic for data words and demonstrates its properties that ensure the decidability of the synthesis problem for distributed systems.

Findings

Decidability of the synthesis problem for systems modeled by data words.

Introduction of prefix first-order logic as a suitable specification language.

Properties of the logic that facilitate synthesis algorithm design.

Abstract

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.