研究带时序逻辑的数据库查询数据复杂度,揭示其计算难度边界。
On Deciding the Data Complexity of Answering Linear Monadic Datalog Queries with LTL Operators(Extended Version)
- 分析带有时序算子的线性一阶递归查询的数据复杂度
- 确定部分算子组合下问题属于AC0、NC¹或LogSpace-hard
- 证明某些情况下复杂度判定不可解,适用于理论计算研究者
本文研究带有线性时序逻辑(LTL)算子的线性一阶递归查询的数据复杂度。首先发现,对于任意连通查询,若使用算子$igcirc/igcirc^-$(下一时刻/前一时刻),其数据复杂度要么在AC0,要么在$ACC0\setminus AC0$,要么是$NC^1$-完全,要么是LogSpace-hard且属于NLogSpace。随后证明:判断此类查询是否为LogSpace-hard的问题是PSpace-complete;而验证是否属于AC0、ACC0或$NC^1$-完全可在ExpSpace内完成。最后,在假设$NC^1 \ne NLogSpace$和$LogSpace \ne NLogSpace$的前提下,证明使用算子$ riangle_f/\triangle_p$(未来/过去某时刻)的查询,其复杂度类归属(AC0、ACC0、$NC^1$-完全、LogSpace-hard)均为不可判定。
原文摘要 · Abstract (English)
Our concern is the data complexity of answering linear monadic datalog queries whose atoms in the rule bodies can be prefixed by operators of linear temporal logic LTL. We first observe that, for data complexity, answering any connected query with operators $\bigcirc/\bigcirc^-$ (at the next/previous moment) is either in AC0, or in $ACC0\!\setminus\!AC0$, or $NC^1$-complete, or LogSpace-hard and in NLogSpace. Then we show that the problem of deciding LogSpace-hardness of answering such queries is PSpace-complete, while checking membership in the classes AC0 and ACC0 as well as $NC^1$-completeness can be done in ExpSpace. Finally, we prove that membership in AC0 or in ACC0, $NC^1$-completeness, and LogSpace-hardness are undecidable for queries with operators $\Diamond_f/\Diamond_p$ (sometime in the future/past) provided that $NC^1 \ne NLogSpace$, and $LogSpace \ne NLogSpace$.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。