The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations

2023/10/14 by Marius Bozga, Lucas Bueri, Bozga, Marius +5
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2310.09542

openalex publication_date 2023/10/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

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
• On the Expressiveness of a Logic of Separated Relations
• Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
• The Tree Width of Separation Logic with Recursive Definitions