2024/02/25 by Lucas Bueri, Bueri, Lucas, Radu Iosif +3
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
paper · pdf · doi:10.48550/arxiv.2402.16150
openalex publication_date 2024/02/25 · openalex created_date 2024/02/28 · openalex updated_date 2026/07/28
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.