1 Search Results for "Stietel, Olivier"


Document
Local First-Order Logic with Two Data Values

Authors: Benedikt Bollig, Arnaud Sangnier, and Olivier Stietel

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)


Abstract
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.

Cite as

Benedikt Bollig, Arnaud Sangnier, and Olivier Stietel. Local First-Order Logic with Two Data Values. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.FSTTCS.2021.39,
  author =	{Bollig, Benedikt and Sangnier, Arnaud and Stietel, Olivier},
  title =	{{Local First-Order Logic with Two Data Values}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{39:1--39:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.39},
  URN =		{urn:nbn:de:0030-drops-155508},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.39},
  annote =	{Keywords: first-order logic, data values, specification of distributed algorithms}
}
  • Refine by Author
  • 1 Bollig, Benedikt
  • 1 Sangnier, Arnaud
  • 1 Stietel, Olivier

  • Refine by Classification
  • 1 Theory of computation → Formal languages and automata theory

  • Refine by Keyword
  • 1 data values
  • 1 first-order logic
  • 1 specification of distributed algorithms

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail