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

翻译：本文研究关系分离逻辑（SLR），并将其表达力与（一元）二阶逻辑（M）SO进行比较。SLR基于著名的分离逻辑符号堆片段，其公式由指向断言和归纳定义谓词组成，并以分离合取作为唯一的逻辑联结词。SLR通过支持一般关系原子（而非仅指向断言）来推广符号堆片段。本文中，我们仅考虑有限关系结构，因此只研究弱（M）SO，其量词限于有限集合。我们的主要结果是：在树宽无界结构上，SLR与MSO不可比较，而SLR总体上可嵌入SO中。此外，当模型的树宽受参数约束且所有附属于某超边的顶点均属于某个固定一元关系符号的解释时，MSO成为SLR的严格子集。我们还讨论了在有界树宽模型上识别与MSO等价的SLR片段的问题。