Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations

Marius Bozga, Lucas Bueri, Radu Iosif, Florian Zuleger

TL;DR

This paper studies the treewidth boundedness problem (TWB) for a generalization of Separation Logic to relational signatures (SLR). It proves undecidability of TWB for first-order logic while establishing decidability for TWB in SLR via a two-step approach: (i) solvability for expandable SIDs with nullary predicates using canonical and RGB-conformant color abstractions, and (ii) a reduction from arbitrary SIDs to expandable ones through a tree-automata framework that manipulates persistent variables. The core contributions are the decidability result for TWB in expandable SLR, the robust automata-based reduction technique, and a clear separation between the decidable SLR fragment and the FO/MSO boundary. The results enable automatic reasoning about the treewidth of graph-like models defined by SLR formulas and support potential decidable entailment fragments, with practical impact on verification and analysis of relational data structures. The work also clarifies the limits of expressivity by showing FO undecidability, strengthening the theoretical understanding of the MSO/ treewidth landscape in logic-based verification.

Abstract

The treewidth boundedness problem for a logic asks for the existence of an upper bound on the treewidth of the models of a given formula in that logic. This problem is found to be undecidable for first order logic. We consider a generalization of Separation Logic over relational signatures, interpreted over standard relational structures, and describe an algorithm for the treewidth boundedness problem in the context of this logic.

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations

TL;DR

This paper studies the treewidth boundedness problem (TWB) for a generalization of Separation Logic to relational signatures (SLR). It proves undecidability of TWB for first-order logic while establishing decidability for TWB in SLR via a two-step approach: (i) solvability for expandable SIDs with nullary predicates using canonical and RGB-conformant color abstractions, and (ii) a reduction from arbitrary SIDs to expandable ones through a tree-automata framework that manipulates persistent variables. The core contributions are the decidability result for TWB in expandable SLR, the robust automata-based reduction technique, and a clear separation between the decidable SLR fragment and the FO/MSO boundary. The results enable automatic reasoning about the treewidth of graph-like models defined by SLR formulas and support potential decidable entailment fragments, with practical impact on verification and analysis of relational data structures. The work also clarifies the limits of expressivity by showing FO undecidability, strengthening the theoretical understanding of the MSO/ treewidth landscape in logic-based verification.

Abstract

The treewidth boundedness problem for a logic asks for the existence of an upper bound on the treewidth of the models of a given formula in that logic. This problem is found to be undecidable for first order logic. We consider a generalization of Separation Logic over relational signatures, interpreted over standard relational structures, and describe an algorithm for the treewidth boundedness problem in the context of this logic.
Paper Structure (49 sections, 37 theorems, 73 equations, 17 figures, 1 table)

This paper contains 49 sections, 37 theorems, 73 equations, 17 figures, 1 table.

Table of Contents

  1. Introduction
  2. Related work
  3. Motivating examples
  4. The Separation Logic of Relations
  5. Structures
  6. Treewdith
  7. Separation Logic of Relations
  8. Simplifying assumptions
  9. The treewidth boundedness problem
  10. Expandable Sets of Inductive Definitions
  11. Canonical models
  12. Expandable sets of inductive definitions
  13. Color schemes
  14. Connected structures
  15. Color abstractions of externally fused sets
  16. ...and 34 more sections

Key Result

Lemma 2.6

Given a SID $\Delta$, one can build an equality-free SID $\Delta'$, such that ${{\bf [\![} {\mathsf{A}} {\bf ]\!]}}_{\Delta} = {{\bf [\![} {\mathsf{A}} {\bf ]\!]}}_{\Delta'}$, for each nullary predicate $\mathsf{A}$. Moreover, all quantitative measures (def:sid-measures) of $\Delta'$ are the same as

Figures (17)

  • Figure 1: Examples of bounded and unbounded treewidth models
  • Figure 2: Composition of structures
  • Figure 3: The syntax (a) and semantics (b) of the Separation Logic of Relations
  • Figure 4: Quotient (a) and internal fusion (b)
  • Figure 5: An expandable SID
  • ...and 12 more figures

Theorems & Definitions (133)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Lemma 2.6
  • proof
  • Proposition 2.7
  • proof
  • Definition 2.8
  • ...and 123 more