归纳关系分离逻辑的树宽有界模型的有效 MSO 可定义性
计算机科学中的逻辑
2024-02-27 v1 形式语言与自动机理论
摘要
一个图语言类在单体二阶逻辑 (MSO) 中是可定义的，当且仅当它由 MSO 公式的模型集合构成。此外，如果此类集合中图的树宽存在可计算的上界，则根据 Courcelle 定理，其可满足性和蕴涵问题是可判定的。这促使我们将其他图逻辑与 MSO 进行比较。在本文中，我们考虑了一种关系分离逻辑 (SLR) 的 MSO 可定义性，该逻辑描述了简单超图，其中每个顶点序列最多附着一条具有给定标签的边。我们的逻辑 SLR 使用归纳谓词，其递归定义由关系原子和谓词原子的存在量化分离合取组成。本文的主要贡献是提出了 SLR 的一个富有表现力的片段，该片段描述了树宽有界的图集合，并且可以有效地转换为 MSO。
引用
@article{arxiv.2402.16150,
title = {Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations},
author = {Lucas Bueri and Radu Iosif and Florian Zuleger},
journal= {arXiv preprint arXiv:2402.16150},
year = {2024}
}