PaperlayerView exact revision on arXiv

Source-linked AI summary

The Tree Width of Separation Logic with Recursive Definitions

Radu Iosif, Adam Rogalewicz, Jiri Simacek

arXiv:1301.5139v2cs.LOcs.FL

TL;DR

Expressive Separation Logic with recursive definitions raises difficult decidability questions, while existing practical fragments often narrow the syntax or restrict models to lists. This paper defines a bounded-tree-width fragment and reduces its decision problems to MSO; satisfiability and entailment are decidable for that fragment, which covers structures beyond lists and trees.

  • Problem

    Expressive Separation Logic with recursive definitions is difficult to decide automatically, and practical dialects often restrict syntax and models, typically to singly linked lists.

    Source: §1 · pp. 1–2

  • Method

    The paper defines SLRDbtw, whose recursive-definition syntax guarantees bounded-tree-width models, and reduces its formulae to MSO over graphs.

    Source: §1 · p. 2

  • Results

    Satisfiability and entailment for SLRDbtw are decidable by reduction to MSO over states of bounded tree width.

    Source: §4.6 · p. 17

  • Takeaways & Limitations

    The fragment describes general unbounded mutable structures, including trees with parent pointers and linked leaves, beyond lists and trees.

    Source: §5 · p. 17

    The decidability argument requires established recursive definitions; unallocated existential variables can produce models with unbounded tree width.

    Source: §3 · p. 9, §3.1 · p. 10

Abstract

from arXiv · show

Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments between such formulae are decidable for validity. These predicates are general enough to define (doubly-) linked lists, trees, and structures more general than trees, such as trees whose leaves are chained in a list. The decidability proofs are by reduction to decidability of Monadic Second Order Logic on graphs with bounded tree width.

1 Introduction

Separation Logic supports compositional reasoning about mutable, dynamically allocated structures, but recursive definitions make automatic decidability difficult. The paper introduces a bounded-tree-width fragment whose satisfiability and entailment are decidable, and relates it to prior logics for lists and more general structures.

1 Introduction

  • SL supports local reasoning over disjoint heap regions, with applications in academic and industrial program-verification tools.It is used as both a property-specification language and an internal domain for computing invariants or proving verification conditions.Source: §1 · p. 1
  • Recursive definitions describe unbounded data structures, while expressive SLRD makes automatic decidability difficult and practical dialects often restrict syntax and models.The commonly considered models are typically singly linked lists and slight variations.Source: §1 · pp. 1–2
  • SLRDbtw restricts recursive-definition syntax so every model has bounded tree width, making satisfiability and entailment decidable without restricting data-structure types.The paper reduces SLRDbtw formulae to MSO over graphs, then uses bounded tree width to obtain decidability through tree-automata emptiness.Source: §1 · p. 2
  • Prior approaches include logics decided through MSO on trees, an enumerative small-model approach, and fragments reduced to MSO on bounded-tree-width graphs,,,.The cited approaches cover routing-expression trees, shape and path-length reasoning, and decidable fragments with quantified data theories.Source: Related Work · p. 2

Related Work

  • Earlier SLRD decidability results focused on singly linked lists [2] or list entailment, later extended to nested and overlaid lists [10].The paper presents SLRDbtw as the first decidable Separation Logic able to define structures beyond lists and trees, including trees with parent pointers and linked leaves.Source: Related Work · pp. 2–3

2 Preliminaries

The preliminaries define the state and tree objects used to model heaps as labeled graphs, then introduce tree decompositions and tree width as a measure of their structure.

2 Preliminaries

  • The notation sets cardinality and partial-function conventions, while pointer variables name locations and selectors label heap edges.The null variable and location are designated, and the selector set is finite.Source: §2 · p. 3, Stores, Heaps and States · p. 3

Stores, Heaps and States.

  • A state pairs a store mapping pointer variables to locations with a finite heap of selector edges; locations referenced but not allocated are dangling.The heap excludes the null location and each allocated location has at least one outgoing selector edge.Source: Stores, Heaps and States · p. 3

Trees.

  • Trees use finite sequences as positions, with child positions formed by appending an index; paths may link siblings but cannot revisit a position.A tree position's parent is obtained by removing its final index.Source: Trees · pp. 3–4

Tree Width.

  • A tree decomposition assigns location sets to tree nodes, covers each state edge in a set, and keeps shared locations along paths; its width is the largest set size minus one.Tree width is the minimum decomposition width; Fig. 2 depicts a graph and a possible decomposition of width 2.Source: Tree Width · p. 4, Figure 2 · p. 4

2.1 Syntax and Semantics of Monadic Second Order Logic

This section defines MSO on states and basic Separation Logic, then gives decidability for MSO satisfiability on states of bounded tree width and a tree-width bound for basic SL models.

2.1 Syntax and Semantics of Monadic Second Order Logic

  • MSO on states adapts labeled-graph MSO, with first-order variables for locations and second-order variables for sets of locations.Its atomic predicates express equality, variable labels, null, set membership, and selector-labeled edges.Source: §2.1 · pp. 4–5
  • MSO satisfiability is decidable when the state models are restricted to tree width at most a fixed constant k.The unrestricted MSO satisfiability problem is described as undecidable.Source: §2.1 · p. 5

2.2 Syntax and Semantics of Separation Logic

  • Basic Separation Logic formulas combine pure constraints, spatial formulas, and existential quantification, with separating conjunction requiring disjoint heap domains.Points-to is interpreted strictly: it specifies one allocated cell with exactly the stated outgoing edges.Source: Basic Formulae · pp. 5–6, §2.2 · p. 5

Basic Formulae.

  • Every model of a basic SL formula ϕ has tree width at most max(|ϕ|, ||PVar||).A variable is allocated when it occurs as the source of a points-to atom; allocated variables cannot refer to dangling locations in models.Source: Basic Formulae · p. 6

Recursive Definitions.

Recursive definitions consist of rules with spatial heads, recursive predicate tails, and pure constraints; finite unfoldings characterize their models and cover structures such as trees with parent pointers and linked leaves.

  • A recursive rule has a spatial head, an ordered sequence of recursive predicate occurrences as its tail, and a pure constraint.Rules with empty tails are base cases; the maximum number of variables in a rule is denoted ||P||var.Source: Recursive Definitions · pp. 6–7
  • The tll predicate describes a binary tree with parent pointers whose leaves are linked left-to-right in a singly linked list.Its base rule allocates leaves, while its recursive rule allocates internal nodes and invokes tll for the left and right subtrees.Source: Recursive Definitions · p. 7
  • An unfolding tree is finite, labels each node with a rule, and gives recursive calls ordered children labeled by applicable rules.The characteristic formula is defined from the rules at the unfolding-tree positions, composing child formulas with the parent rule.Source: Recursive Definitions · pp. 7–8
  • A recursive predicate with no finite unfolding tree, such as P(x) ::= ∃y . x 7→y ∗P(y), makes ∃x.P(x) unsatisfiable.Source: Recursive Definitions · p. 8
  • An SLRD formula existentially quantifies a basic formula conjoined by separating conjunction with recursive-predicate occurrences.Source: Top Level Formulae · p. 8

Top Level Formulae.

Top-level SLRD formulae combine basic formulae with recursive predicates; the section defines satisfiability and entailment and notes that entailment cannot be reduced directly to satisfiability within this fragment.

  • The example formulae describe binary trees with parent pointers and linked leaves, while ϕ1 additionally permits a tree with only one allocated location.Source: Top Level Formulae · pp. 8–9
  • Satisfiability asks whether a closed formula has a model, while entailment asks whether every model of one closed formula is also a model of another.The notation ϕ1 |=sl ϕ2 expresses entailment.Source: Top Level Formulae · p. 9
  • Entailment cannot be reduced directly to satisfiability here because SLRD is not closed under negation.Source: Top Level Formulae · p. 9

3 Decidability of Satisfiability and Entailment in SLRD

Under natural restrictions on recursive definitions, SLRDbtw guarantees bounded-tree-width models; translating its formulas to MSO then yields decidability for satisfiability and entailment.

3 Decidability of Satisfiability and Entailment in SLRD

  • The three restrictions define the SLRDbtw fragment, whose model tree width is bounded under the stated conditions.Source: §3 · p. 9, §3.1 · p. 9
  • SLRDbtw satisfiability and entailment are decided by translating formulas to equivalent MSO formulas and using decidability on bounded-tree-width states.Source: §3 · p. 9

3.1 A Decidable Subset of SLRD

  • Progress requires each recursive rule to allocate exactly one variable in its head.Source: §3.1 · p. 9, §3 · p. 9
  • Connectivity requires each recursive child to be linked by a selector edge to the variable allocated by its parent rule.Source: §3.1 · p. 10
  • Establishment requires every existentially quantified variable to be eventually allocated; otherwise dangling selectors can produce squared-grid models with unbounded tree width.Source: §3.1 · p. 10
  • Models of an established recursive-definition system have tree width at most the system's number of variables.Source: §3.1 · p. 11
  • Top-level SLRDbtw models have tree width bounded by the maximum of the quantified-variable count, basic-formula size, pointer-variable count, and predicate-system size.Source: §3.1 · p. 11

4 From SLRDbtw to MSO

This section translates basic and recursively defined Separation Logic formulae, including SLRDbtw parameters, into MSO, using unfolding-tree structure and routing automata to capture edges, prevent double allocation, and handle predicate parameters. It establishes semantic correspondence and derives decidability of satisfiability and entailment by reduction to MSO on states of bounded tree width.

4.1 Converting Basic SL Formulae to MSO

  • The MSO translation of a basic SL formula defines exactly the same models as the original formula.Lemma 3 states equivalence for every state, interpretation, and basic SL formula.Source: §4.1 · pp. 11–12

4.2 States and Backbones

  • Recursive-predicate models are encoded through an unfolding tree whose heap allocation is bijective, with a backbone of local edges and MSO constraints enforcing rule-consistent labels and outgoing edges.The encoding also ensures locations have no more outgoing edges than the rule head specifies, since MSO semantics does not impose SL’s strictness conditions.Source: §4.2 · pp. 12–13

4.3 Inner Edges

  • Inner edges are encoded by recognizing paths of equalities in the unfolding tree with tree-walking automata, and Lemma 4 establishes the automata’s correctness.The path conditions apply to edges between allocated locations; edges to dangling locations are handled separately in Appendix 4.5.Source: §4.3 · pp. 13–14

4.4 Double Allocation

  • A sanity constraint rules out double allocation by requiring that every run of the detecting automaton marks the same tree position as its start and end.A run marking distinct positions exists exactly when two positions allocate the same location.Source: §4.4 · pp. 15–16

4.5 Handling Parameters

  • For each top-level predicate parameter, modified routing automata track its equalities through the unfolding tree and distinguish whether it is allocated, referenced, or another parameter.The parameter’s assignment is expressed by MSO constraints.Source: §4.5 · pp. 16–17
  • SL parameters xi,j correspond to first-order MSO variables, and parami,j is formed by conjoining paramc constraints for c = 1, 2, 3.Source: §4.5 · p. 17

4.6 Translating Top Level SLRDbtw Formulae to MSO

  • Lemma 5 states that a recursively defined predicate holds in a state exactly when its MSO translation holds under corresponding interpretations.The interpretations agree on SL variables, with first-order variables valued in locations and second-order variables in sets of locations.Source: §4.6 · p. 17
  • The top-level translation handles formulas of the form ∃z . φ(y0) ∗ Pi1(y1) ∗ ...Pik(yk), with each yj drawn from z.Theorem 3 gives an MSO equivalence for any closed SLRDbtw formula.Source: §4.6 · p. 17
  • Theorem 2 and Theorem 3 yield decidability of SLRDbtw satisfiability and entailment by reduction to MSO over states of bounded tree width.Theorem 3 establishes an MSO correspondence for closed SLRDbtw formulas.Source: §4.6 · p. 17

5 Conclusions and Future Work

The paper defines a decidable fragment of Separation Logic with Recursive Definitions for general unbounded mutable structures, and leaves tight complexity bounds for future work.

  • The fragment covers general unbounded mutable structures, including trees with parent pointers and linked leaves.Source: §5 · p. 17
  • Satisfiability and entailment are decidable by reduction to MSO over graphs of bounded tree width.Source: §5 · p. 17
  • The authors conjecture that the decision problems have elementary complexity and plan to compute tight upper bounds.Source: §5 · p. 17

A Definition of tree structures in MSO

The MSO definition represents a tree using labeled nodes and partial successor functions, then constrains the structure to be rooted, tree-shaped, and reachable from its root.

B Standard Tree Walking Automata

The section defines tree-walking automata and accepting runs, then shows that standard tree-walking automata can simulate the more general form without changing the accepted trees.

C MSO encoding of Tree Walking Automata

The MSO encoding marks tree positions by automaton states and constrains a run from the root to a final position; its correctness is characterized by an equivalent loop-free accepting run.

D Routing Automaton Example

The example instantiates a routing automaton for predicatetll, the tree-with-link-leaves predicate, and lays out its transition relation by numbered cases.

D Routing Automaton Example

E Missing Proofs

The missing proofs establish the MSO-based decidability argument by relating separation-logic satisfaction to MSO satisfaction and bounding the tree width of states from formulas and predicate unfoldings. They also prove extension invariance and justify the translation, including the basic formula and separating-conjunction cases.

E Missing Proofs

  • Theorem 1 reduces MSO satisfiability over states to arbitrary-graph MSO using three MSO state restrictions, yielding decidability via.The restrictions encode unique pointer-variable locations, at most one target per edge, and a unique nil location with no outgoing edges.Source: E Missing Proofs · pp. 23–24
  • The base-state decomposition has bags bounded by max(|ϕ|, ||PVar||), while unfolding-tree bags are bounded by the variables occurring in each rule.For the base state, allocated and target locations occupy the repeated bags, with pointer-variable images in the root bag; unfolding-tree bags contain locations associated with free or existentially quantified variables.Source: E Missing Proofs · pp. 24–25
  • Combining the base state and recursive-predicate components yields a decomposition bounded by max(||z||, |ϕ|, ||PVar||, ||P||var).The proof joins component decompositions beneath a root bag containing the locations assigned to z.Source: E Missing Proofs · pp. 25–26
  • The MSO predicate Heap(X) denotes exactly dom(h), and translations of basic spatial formulas preserve truth under disjoint state extensions.The proofs use the heap-domain characterization and induction on the formula structure, including separating conjunction.Source: E Missing Proofs · p. 26
  • For adjacent or identical unfolding-tree positions, equality between their variables holds exactly when the automaton can move between the corresponding states in one step.The proof extends this correspondence along paths in the unfolding tree.Source: E Missing Proofs · p. 27
  • The converse construction builds an unfolding tree from the MSO backbone and parameter conditions, then extends the variable assignment to satisfy its SL formula.The proof uses the one-to-one correspondence between predicate rules and variables to label the tree, and assigns locations consistently with equalities in the unfolded formula.Source: E Missing Proofs · p. 29
  • Lemma 10 shows that the stated MSO conditions for a predicate remain equivalent after extending the state with a disjoint heap.The conditions include backbone, inner allocation, and parameter predicates.Source: E Missing Proofs · p. 30
  • For the basic separation-logic formula, the proof uses Lemma 3 and Heap(X) to relate satisfaction to an MSO formula over the heap domain.It uses Proposition 1 to identify the set of locations X with dom(h).Source: E Missing Proofs · pp. 30–31
  • For an interpretation meeting the requirements of Lemmas 3 and 5, applying Lemmas 9 and 10 supports the separating-conjunction result; conversely, the heap splits into disjoint parts.The restrictions h1 and h2 to disjoint L1 and L2 form S = S1 ⊎ S2, and the cited passage concludes S |=sl ∃z . φ(y0) ∗ P(y1).Source: E Missing Proofs · p. 31
Loading 1301.5139v2…