论文标题
关于分离关系的逻辑的表现力
On the Expressiveness of a Logic of Separated Relations
论文作者
论文摘要
我们比较了分离逻辑存在的模型理论表达于不受限制的关系特征（SLR） - 仅将连词分开为逻辑结缔组织和高阶归纳定义，传统上称为符号堆片段 - 具有（Monadic）第二阶逻辑（（M）的表达性（（M））。尽管SLR和MSO在无界树宽的结构上是无与伦比的，但事实证明SLR通常可以嵌入SO中，并且当模型的树宽受到以输入为输入的参数时，MSO成为SLR的严格子集。我们还讨论了定义SLR片段的问题，该片段等效于MSO，而不是有限的树宽模型。然后，这种片段将成为具有可决定性问题的最通用的分离逻辑，这是基于（可重构）基于组件和分布式系统的实际验证方法的关键要素。
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.
