Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Satisfiability of Local First-Order Logics with Data

Benedikt Bollig, Arnaud Sangnier, Olivier Stietel

TL;DR

This work analyzes satisfiability for local first-order logics with data on unordered structures, introducing radius-bounded local fragments. It proves a decidability result for the local radius-$1$ fragment with one diagonal relation, and shows undecidability for any larger radius, establishing a sharp frontier. It then delivers a precise landscape for existential fragments parameterized by data-arity and radius, including tight upper and lower bounds and tiling-based reductions. The results provide a map of decidable versus undecidable formalisms for data-rich specifications and furnish techniques (e.g., well-typed models and ext-dFO$^{2}$ reductions) for reasoning about distributed systems with data.

Abstract

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we introduce a family of local fragments. They restrict quantification to the neighbourhood of a given reference point that is bounded by some radius. Our first main result establishes decidability of the satisfiability problem for the local radius-1 fragment in presence of one "diagonal relation". On the other hand, extending the radius leads to undecidability. In a second part, we provide the precise decidability and complexity landscape of the satisfiability problem for the existential fragments of local logic, which are parameterized by the number of data values carried by each element and the radius of the considered neighbourhoods. Altogether, we draw a landscape of formalisms that are suitable for the specification of systems with data and open up new avenues for future research.

On the Satisfiability of Local First-Order Logics with Data

TL;DR

This work analyzes satisfiability for local first-order logics with data on unordered structures, introducing radius-bounded local fragments. It proves a decidability result for the local radius- fragment with one diagonal relation, and shows undecidability for any larger radius, establishing a sharp frontier. It then delivers a precise landscape for existential fragments parameterized by data-arity and radius, including tight upper and lower bounds and tiling-based reductions. The results provide a map of decidable versus undecidable formalisms for data-rich specifications and furnish techniques (e.g., well-typed models and ext-dFO reductions) for reasoning about distributed systems with data.

Abstract

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we introduce a family of local fragments. They restrict quantification to the neighbourhood of a given reference point that is bounded by some radius. Our first main result establishes decidability of the satisfiability problem for the local radius-1 fragment in presence of one "diagonal relation". On the other hand, extending the radius leads to undecidability. In a second part, we provide the precise decidability and complexity landscape of the satisfiability problem for the existential fragments of local logic, which are parameterized by the number of data values carried by each element and the radius of the considered neighbourhoods. Altogether, we draw a landscape of formalisms that are suitable for the specification of systems with data and open up new avenues for future research.
Paper Structure (24 sections, 39 theorems, 39 equations, 6 figures, 1 table)

This paper contains 24 sections, 39 theorems, 39 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Related Work.
  3. Outline.
  4. Structures and First-Order Logic
  5. Data Structures
  6. First-Order Logic
  7. Local First-Order Logic
  8. Previously Known Results
  9. 0 and 1 Data Value
  10. A Normal Form
  11. Extended Two-Variable First-Order Logic
  12. Dealing with Two Data Values
  13. Decidability with Radius One and One Diagonal Relation
  14. Undecidability results
  15. The Tiling Problem
  16. ...and 9 more sections

Key Result

Theorem 2.2

The problem $\textsc{DataSat}(\textup{dFO},2,\{{_{1}{\sim_{1}}},{_{2}{\sim_{2}}}\})$ is undecidable, even when we require that $\Sigma = \emptyset$.

Figures (6)

  • Figure 3: (a) A data structure over $\Sigma = \emptyset$. (b) Adding unary predicates for a given element $a$. (c) Adding counting constraints to $a$. (d) A well-typed data structure from $\textup{Data}[\{\mathsf{eq}\} \cup \mathtt{C}_{3}]$.
  • Figure 4: (a) Adding diagonal elements. (a)$\leftarrow$(b) Making a data structure eq-respecting with the following permutation on the first element $1\mapsto 2, 2 \mapsto 4, 3\mapsto 1, 4 \mapsto 3$.
  • Figure 5: Counting intersections for $M = 3$ and elements with label $\mathsf{p}$
  • Figure 6: The local pattern of $\mathfrak{A}_{2m}$. Dots denote elements. Two dots are in the same $\mathrel{_{1}{\sim}{_{1}}}$-equivalence class (resp. $\mathrel{_{2}{\sim}{_{2}}}$) iff they are in the same green (resp. purple) area. The thick black lines represent the relation $\mathrel{_{1}{\sim}{_{2}}}$ in the following way: if a $\mathrel{_{1}{\sim}{_{1}}}$-equivalence class $C_1$ and a $\mathrel{_{2}{\sim}{_{2}}}$-equivalence class $C_2$ are connected with a thick black line, then for any $a\in C_1$ and $b\in C_2$, we have $a \mathrel{_{1}{\sim}{_{2}}} b$.
  • Figure 7: Some 3-local views of $\mathfrak{A}_{2m}$ for $\Gamma=\{(1,1),(2,2)\}$.
  • ...and 1 more figures

Theorems & Definitions (75)

  • Example 2.1
  • Theorem 2.2: Janiczak-Undecidability-fm53
  • Example 2.3
  • Theorem 2.4: borger-classical-springer97etessami-first-ic02
  • Theorem 2.5: Mundhenk09Fitting12
  • Lemma 2.6
  • Theorem 2.7: KieronskiT09
  • Proposition 2.8
  • proof
  • Example 3.1
  • ...and 65 more