On the Expressiveness of a Logic of Separated Relations

TL;DR

This paper analyzes the expressiveness of a fragment of Separation Logic compared to Monadic Second Order Logic, revealing their relationships and potential for decidable verification over models with bounded treewidth.

Contribution

It establishes the embedding of SLR into SO and characterizes the expressiveness relationship between MSO and SLR based on model treewidth, proposing a fragment with decidable entailment.

Findings

SLR can be embedded in SO logic.

MSO is a strict subset of SLR for bounded treewidth models.

A fragment of SLR equivalent to MSO could enable decidable verification.

Abstract

We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) -- with only separating conjunction as logical connective and higher-order inductive definitions, traditionally known as the symbolic heap fragment -- with the expressiveness of (Monadic) Second Order Logic ((M)SO). While SLR and MSO are incomparable on structures of unbounded treewidth, it turns out that SLR can be embedded in SO, in general, and that MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter given as input. We also discuss the problem of defining a fragment of SLR that is equivalent to MSO over models of bounded treewidth. Such a fragment would then become the most general Separation Logic with a decidable entailment problem, a key ingredient of practical verification methods for self-adapting (reconfigurable) component-based and distributed systems.