守护片段邂逅动态逻辑：正则守护的故事（扩展版）
计算机科学中的逻辑
2025-09-12 v1
摘要
我们研究了带有正则守护的守护片段（RGF），该逻辑将守护片段（GF）的表现力与带有交叉和逆转的命题动态逻辑（ICPDL）相结合。我们的逻辑以统一的方式概括了许多此前研究的 GF 的扩展，包括（或的）传递或等价守护、传递或等价闭包等。我们证明了 RGF 满足问题的 2EXPTIME 可判定性，表明 RGF 不比 ICPDL 或 GF 更难。转向查询蕴涵问题，我们提供显著加强和巩固此前结果的不可判定性结果。我们通过识别 RGF 的一个自然意义上的最大 EXPSPACE 可判定片段来作结。
引用
@article{arxiv.2509.09218,
title = {Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version)},
author = {Bartosz Bednarczyk and Emanuel Kieroński},
journal= {arXiv preprint arXiv:2509.09218},
year = {2025}
}
备注
This is an extended version of our paper that will appear at KR 2025. The current appendix has not yet been revised; an updated version will be released in the near future