On the Expressiveness of a Logic of Separated Relations

2022/08/02 by Radu Iosif, Iosif, Radu, Florian Zuleger +1
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Semantic Web and Ontologies #Service-Oriented Architecture and Web Services

paper · pdf · doi:10.48550/arxiv.2208.01520

openalex publication_date 2022/08/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Expressiveness Results for an Inductive Logic of Separated Relations
• Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
• The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
• Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
• A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions