On the Expressiveness of a Logic of Separated Relations
share
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.
READ FULL TEXT