正则语言与线性时序逻辑中本体介导查询的 FO-可重写性判定
计算复杂性
2023-03-16 v2 计算机科学中的逻辑
摘要
我们所关注的问题是确定在 (Z,<) 上以线性时序逻辑 LTL 表述的本体介导查询（OMQ）回答的数据复杂度，并判定其是否可重写为 FO(<)-查询（可能带某些额外谓词）。首先，我们观察到，与正则语言的电路复杂度和 FO-可定义性一致，AC^0、ACC^0 与 NC^1 中的 OMQ 回答分别等价于使用一元谓词 x \equiv 0 (mod n) 的 FO(<,\equiv)-可重写性、FO(<,MOD)-可重写性，以及使用关系原语递归的 FO(RPR)-可重写性。我们证明，类似于已知的识别正则语言 FO(<)-可定义性的 PSPACE-完全性，判定 FO(<,\equiv)- 与 FO(<,MOD)-可定义性也是 \PSPACE-完全的（除非 ACC^0 = NC^1）。我们随后利用该结果证明，判定 LTL OMQ 的 FO(<)-、FO(<,\equiv)- 与 FO(<,MOD)-可重写性是 EXPSPACE-完全的，且这些问题对于带线性 Horn 本体与原子查询的 OMQ 变为 PSPACE-完全，在 FO(<)- 与 FO(<,\equiv)-可重写性情形下带正查询时亦如此。进一步，我们考虑带二文字本体的 OMQ 的 FO(<)-可重写性，并识别出判定其为 PSPACE-、Pi_2^p- 与 coNP-完全的 OMQ 类。
引用
@article{arxiv.2207.06210,
title = {Deciding FO-rewritability of regular languages and ontology-mediated queries in Linear Temporal Logic},
author = {Agi Kurucz and Vladislav Ryzhikov and Yury Savateev and Michael Zakharyaschev},
journal= {arXiv preprint arXiv:2207.06210},
year = {2023}
}
备注
arXiv admin note: text overlap with arXiv:2105.06202