Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913244197683200 |
|---|---|
| author | Bueri, Lucas Iosif, Radu Zuleger, Florian |
| author_facet | Bueri, Lucas Iosif, Radu Zuleger, Florian |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_16150 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations Bueri, Lucas Iosif, Radu Zuleger, Florian Logic in Computer Science Formal Languages and Automata Theory 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. |
| title | Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2402.16150 |