Local First-Order Logic with Two Data Values

Benedikt Bollig (1) , Arnaud Sangnier (2) , Olivier Stietel (2, 1)

1 LMF - Laboratoire Méthodes Formelles
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale

We study first-order logic over unordered structures whose elements carry two data values from an infinite domain. Data values can be compared wrt. equality so that the formalism is suitable to specify the input-output behavior of various distributed algorithms. As the logic is undecidable in general, we introduce a family of local fragments that restrict quantification to neighborhoods of a given reference point. Our main result establishes decidability of the satisfiability problem for one of these non-trivial local fragments. On the other hand, already slightly more general local logics turn out to be undecidable. 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.

Domaines: Théorie et langage formel [cs.FL]

Benedikt Bollig, Arnaud Sangnier, Olivier Stietel. Local First-Order Logic with Two Data Values. 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), Dec 2021, Goa, India. pp.39:1-39:15. ⟨hal-03353214⟩