Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations

Lucas Bueri, Radu Iosif, Florian Zuleger

TL;DR

The paper investigates how to obtain MSO-definability for graph languages described by a Separation Logic of Relations (SLR) with inductive definitions, under bounded tree-width. It introduces a regular, rigid fragment of SLR whose models have computable, bounded tree-width and can be translated into MSO via MSO-definable transductions and canonical-model constructions, leveraging HR-grammars and fusion/fission operations. A key result shows that, for regular and rigid SID, the SLR models are MSO-definable and have an effectively computable tree-width bound, enabling entailment decidability within this fragment; the approach relies on Backwards Translation to transfer definability from canonical models to general models. The work advances the understanding of translating constructive graph representations into MSO under width bounds, with practical implications for automated verification of graph-structured systems, while noting open questions about the MSO-definability of the fission operation in general.

Abstract

A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound on the tree-widths of the graphs in each such set, the satisfiability and entailment problems are decidable, by Courcelle's Theorem. This motivates the comparison of other graph logics to MSO. In this paper, we consider the MSO definability of a Separation Logic of Relations (SLR) that describes simple hyper-graphs, in which each sequence of vertices is attached to at most one edge with a given label. Our logic SLR uses inductive predicates whose recursive definitions consist of existentially quantified separated conjunctions of relation and predicate atoms. The main contribution of this paper is an expressive fragment of SLR that describes bounded tree-width sets of graphs which can, moreover, be effectively translated into MSO.

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations

TL;DR

The paper investigates how to obtain MSO-definability for graph languages described by a Separation Logic of Relations (SLR) with inductive definitions, under bounded tree-width. It introduces a regular, rigid fragment of SLR whose models have computable, bounded tree-width and can be translated into MSO via MSO-definable transductions and canonical-model constructions, leveraging HR-grammars and fusion/fission operations. A key result shows that, for regular and rigid SID, the SLR models are MSO-definable and have an effectively computable tree-width bound, enabling entailment decidability within this fragment; the approach relies on Backwards Translation to transfer definability from canonical models to general models. The work advances the understanding of translating constructive graph representations into MSO under width bounds, with practical implications for automated verification of graph-structured systems, while noting open questions about the MSO-definability of the fission operation in general.

Abstract

A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound on the tree-widths of the graphs in each such set, the satisfiability and entailment problems are decidable, by Courcelle's Theorem. This motivates the comparison of other graph logics to MSO. In this paper, we consider the MSO definability of a Separation Logic of Relations (SLR) that describes simple hyper-graphs, in which each sequence of vertices is attached to at most one edge with a given label. Our logic SLR uses inductive predicates whose recursive definitions consist of existentially quantified separated conjunctions of relation and predicate atoms. The main contribution of this paper is an expressive fragment of SLR that describes bounded tree-width sets of graphs which can, moreover, be effectively translated into MSO.
Paper Structure (15 sections, 8 theorems, 19 equations, 4 figures)

This paper contains 15 sections, 8 theorems, 19 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contribution
  4. Preliminaries
  5. Graphs
  6. Trees
  7. Graph Grammars
  8. Logics
  9. Monadic Second Order Logic
  10. Separation Logic of Relations
  11. MSO-definability of SLR
  12. An MSO-Definable Fragment of SLR
  13. Canonical Models
  14. MSO-Definable Transductions
  15. Parsable Sets of Canonical Models

Key Result

lemma thmcounterlemma

Let $G,H\in \mathcal{G}^c({\mathbb{A}})$ be isomorphic c-graphs. Then, $G \in {{\bf [\![} {\mathsf{A}} {\bf ]\!]}}^{\mathsf{c}}_{\Delta} \iff H \in {{\bf [\![} {\mathsf{A}} {\bf ]\!]}}^{\mathsf{c}}_{\Delta}$.

Figures (4)

  • Figure 1: Graph operations: composition (a) parallel composition (b) substitution (c) fusion (d)
  • Figure 2: Derivation (left) and parse (right) trees
  • Figure 3: Logics
  • Figure 4: Regular SIDs with productive only (a) and both productive and unproductive (b) rules

Theorems & Definitions (23)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: CourcelleV
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • ...and 13 more