License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.20
URN: urn:nbn:de:0030-drops-190146
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19014/
Go to the corresponding LIPIcs Volume Portal

Iosif, Radu ; Zuleger, Florian

Expressiveness Results for an Inductive Logic of Separated Relations

pdf-format:
LIPIcs-CONCUR-2023-20.pdf (0.9 MB)

Abstract

In this paper we study a Separation Logic of Relations (SLR) and compare its expressiveness to (Monadic) Second Order Logic [(M)SO]. SLR is based on the well-known Symbolic Heap fragment of Separation Logic, whose formulæare composed of points-to assertions, inductively defined predicates, with the separating conjunction as the only logical connective. SLR generalizes the Symbolic Heap fragment by supporting general relational atoms, instead of only points-to assertions. In this paper, we restrict ourselves to finite relational structures, and hence only consider Weak (M)SO, where quantification ranges over finite sets. Our main results are that SLR and MSO are incomparable on structures of unbounded treewidth, while SLR can be embedded in SO in general. Furthermore, MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter and all vertices attached to some hyperedge belong to the interpretation of a fixed unary relation symbol. We also discuss the problem of identifying a fragment of SLR that is equivalent to MSO over models of bounded treewidth.

BibTeX - Entry

@InProceedings{iosif_et_al:LIPIcs.CONCUR.2023.20,
  author =	{Iosif, Radu and Zuleger, Florian},
  title =	{{Expressiveness Results for an Inductive Logic of Separated Relations}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19014},
  URN =		{urn:nbn:de:0030-drops-190146},
  doi =		{10.4230/LIPIcs.CONCUR.2023.20},
  annote =	{Keywords: Separation Logic, Model Theory, Monadic Second Order Logic, Treewidth}
}

Keywords: Separation Logic, Model Theory, Monadic Second Order Logic, Treewidth
Collection: 34th International Conference on Concurrency Theory (CONCUR 2023)
Issue Date: 2023
Date of publication: 07.09.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI