Benedikt Bollig ; Arnaud Sangnier ; Olivier Stietel - On the Satisfiability of Local First-Order Logics with Data

lmcs:11538 - Logical Methods in Computer Science, July 2, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:1)2024
On the Satisfiability of Local First-Order Logics with DataArticle

Authors: Benedikt Bollig ; Arnaud Sangnier ; Olivier Stietel

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.


Volume: Volume 20, Issue 3
Secondary volumes: Selected Papers of the 13th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2022)
Published on: July 2, 2024
Accepted on: April 12, 2024
Submitted on: July 4, 2023
Keywords: Computer Science - Logic in Computer Science
Funding:
    Source : OpenAIRE Graph
  • FoRmal mEthods for the Design of Distributed Algorithms; Funder: French National Research Agency (ANR); Code: ANR-17-CE40-0013

Classifications

Mathematics Subject Classification 20201

1 Document citing this article

Consultation statistics

This page has been seen 3105 times.
This article's PDF has been downloaded 840 times.