The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations

Marius Bozga (1) , Lucas Bueri (1) , Radu Iosif (1) , Florian Zuleger (2)

1 VERIMAG - IMAG - VERIMAG
2 Universität Wien = University of Vienna

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.

Mots clés: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL); FOS: Computer and information sciences

Domaines: Informatique [cs]

Marius Bozga, Lucas Bueri, Radu Iosif, Florian Zuleger. The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. 2023. ⟨hal-04264291v1⟩