Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesis for prefix first-order logic on data words

Julien Grange, Mathieu Lehaut

TL;DR

This paper addresses reactive synthesis for distributed systems with an unbounded number of participants by modeling executions as data words and specifying behavior in prefix first-order logic FO^{pref}[ackslashsim]. It develops a hierarchy of token games and a double-cutoff technique to reduce the potentially infinite search space to a finite, computable one, establishing decidability of synthesis for FO^{pref}[ackslashsim]. Central to the approach are the FO^{pref}-type abstractions forming a tree, Ehrenfeucht-Fraïssé style characterizations, and a ghost-token construction that preserves acceptance while bounding resources. The results narrow the gap between decidable and undecidable logics in data-word synthesis and provide a framework for algorithmic synthesis with unbounded process counts, while leaving open decidability for the full FO[ackslashsim] logic.

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.

Synthesis for prefix first-order logic on data words

TL;DR

This paper addresses reactive synthesis for distributed systems with an unbounded number of participants by modeling executions as data words and specifying behavior in prefix first-order logic FO^{pref}[ackslashsim]. It develops a hierarchy of token games and a double-cutoff technique to reduce the potentially infinite search space to a finite, computable one, establishing decidability of synthesis for FO^{pref}[ackslashsim]. Central to the approach are the FO^{pref}-type abstractions forming a tree, Ehrenfeucht-Fraïssé style characterizations, and a ghost-token construction that preserves acceptance while bounding resources. The results narrow the gap between decidable and undecidable logics in data-word synthesis and provide a framework for algorithmic synthesis with unbounded process counts, while leaving open decidability for the full FO[ackslashsim] logic.

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.
Paper Structure (20 sections, 8 theorems, 41 equations, 3 figures)

This paper contains 20 sections, 8 theorems, 41 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Prefix first-order logic
  3. Data words and preliminaries
  4. Prefix first-order logic on data words
  5. Properties of $\textsc{FO}^{\textsc{pref}}$ types
  6. Synthesis and token games
  7. Standard synthesis game
  8. Symmetric game
  9. Token game on words
  10. Token game on types
  11. Double cutoff for solving the synthesis problem
  12. Having more tokens makes things easier for Environment
  13. Too many tokens are useless to System
  14. Idea of the proof and definitions.
  15. Statement of the invariants.
  16. ...and 5 more sections

Key Result

Proposition 4

Let $k$ be an integer, and let $\mathfrak{w}$, $\mathfrak{\widehat{w}}$ be two data words on the same alphabet (with constants). Then $\mathfrak{w}\xspace\equiv^{\text{pref-EF}}_{k}\xspace\mathfrak{\widehat{w}}\xspace$ if and only if $\mathfrak{w}\xspace\equiv^{\textsc{FO}^{\textsc{pref}}\xspace[\le

Figures (3)

  • Figure 1: A partial representation of $\mathrm{Types}_{\textsc{FO}^{\textsc{pref}}\xspace}^{2}$ for $\Sigma\xspace_E\xspace=\{a_E\xspace\}$ and $\Sigma\xspace_S\xspace=\{a_S\xspace\}$. Types of words containing both $a_E$ and $a_S$ have been omitted, as data classes cannot have such a type.
  • Figure 2: System may need at least as many tokens as Environment to win.
  • Figure 3: Bounding the search space for winning pairs.

Theorems & Definitions (19)

  • Example 1
  • Example 2
  • Definition 3
  • Proposition 4
  • proof
  • Lemma 5
  • proof
  • corollary 1
  • corollary 2
  • Theorem 6
  • ...and 9 more