要約
私たちの懸念は、ルール本体内のアトムに線形時相論理 LTL の演算子をプレフィックスとして付けることができる線形モナディック データログ クエリに応答する際のデータの複雑さです。
まず、データの複雑さのために、演算子 $\bigcirc/\bigcirc^-$ を使用した接続されたクエリへの応答 (次の瞬間/前の瞬間) が AC0 または $ACC0\!\setminus\!AC0$ のいずれかであることがわかります。
または $NC^1$-complete、または LogSpace-hard および NLogSpace 内。
次に、そのようなクエリに答える LogSpace の難易度を決定する問題は PSpace 完全である一方、クラス AC0 および ACC0 のメンバーシップと $NC^1$ 完全性のチェックは ExpSpace で実行できることを示します。
最後に、$NC^ が条件の場合、演算子 $\Diamond_f/\Diamond_p$ を使用したクエリでは、AC0 または ACC0 のメンバーシップ、$NC^1$-完全性、および LogSpace-hardness が (将来/過去のいつか) 決定できないことを証明します。
1 \ne NLogSpace$、および $LogSpace \ne NLogSpace$。
要約(オリジナル)
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$.
arxiv情報
| 著者 | Alessandro Artale,Anton Gnatenko,Vladislav Ryzhikov,Michael Zakharyaschev |
| 発行日 | 2025-01-23 15:41:48+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google