Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Deciding the Data Complexity of Answering Linear Monadic Datalog Queries with LTL Operators(Extended Version)

Alessandro Artale, Anton Gnatenko, Vladislav Ryzhikov, Michael Zakharyaschev

TL;DR

This work analyzes the data complexity of answering temporal monadic Datalog queries with LTL operators, focusing on linear, connected fragments. It shows that for next/previous operators, data complexity falls into $\text{AC}^{0}$, $\text{ACC}^{0} \setminus \text{AC}^{0}$, $\text{NC}^{1}$-complete, or $\text{NL}$-hard, with LogSpace-hardness decisions being $\text{PSPACE}$-complete and membership questions decidable in $\text{ExpSpace}$. The authors prove that Diamond-based operators lead to undecidability for these membership classifications under standard complexity separations. They develop an automata-theoretic framework, including expansions and regular languages over an enlarged alphabet, enabling a decomposition of connected LM$^{\bigcirc}$ queries into plain Datalog and plain LTL parts and yielding an NL data-complexity bound. These results illuminate the interplay between temporal and relational dimensions, offer a tractable core via the linear/monadic fragment, and raise open questions about extending to non-linear, disconnected, or Diamond-rich settings and connections to CSPs and streaming contexts.

Abstract

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$.

On Deciding the Data Complexity of Answering Linear Monadic Datalog Queries with LTL Operators(Extended Version)

TL;DR

This work analyzes the data complexity of answering temporal monadic Datalog queries with LTL operators, focusing on linear, connected fragments. It shows that for next/previous operators, data complexity falls into , , -complete, or -hard, with LogSpace-hardness decisions being -complete and membership questions decidable in . The authors prove that Diamond-based operators lead to undecidability for these membership classifications under standard complexity separations. They develop an automata-theoretic framework, including expansions and regular languages over an enlarged alphabet, enabling a decomposition of connected LM queries into plain Datalog and plain LTL parts and yielding an NL data-complexity bound. These results illuminate the interplay between temporal and relational dimensions, offer a tractable core via the linear/monadic fragment, and raise open questions about extending to non-linear, disconnected, or Diamond-rich settings and connections to CSPs and streaming contexts.

Abstract

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 (at the next/previous moment) is either in AC0, or in , or -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 -completeness can be done in ExpSpace. Finally, we prove that membership in AC0 or in ACC0, -completeness, and LogSpace-hardness are undecidable for queries with operators (sometime in the future/past) provided that , and .
Paper Structure (9 sections, 16 theorems, 24 equations, 3 figures)

This paper contains 9 sections, 16 theorems, 24 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Temporal Datalog
  4. Expansions for Linear Monadic Queries.
  5. Undecidability for Queries with $\raisebox{0.1ex}{\small{$\Diamond$}}\xspace$
  6. Automata-Theoretic Tools for Queries with $\raisebox{0.25ex}{\scriptsize{$\bigcirc$}}$
  7. Decidability for Connected Linear Queries with $\raisebox{0.25ex}{\scriptsize{$\bigcirc$}}$
  8. Conclusions and Future Work
  9. Proofs for Section \ref{['sec:preliminaries']}

Key Result

Proposition 1

For a temporal CQ $Q(X_1, \dots, X_k)$, checking $\mathcal{D}\xspace, \ell \models Q(d_1, \dots, d_k)$ is in $\textsc{AC}^{0}$ for data complexity.

Figures (3)

  • Figure 1: Illustrations for the query $(\pi_1, \textit{Success})$.
  • Figure 2: Illustrations for the query $\{\ref{['rule:pure-datalog-recursive']}, \ref{['rule:pure-datalog-initial-bounded']}\}, G)$ of Example \ref{['ex:pure-datalog-un-bounded']}.
  • Figure 3: Expansions of $\textsl{datalog}_m^{\,{\raisebox{0pt}{$\bigcirc$}}}$ queries.

Theorems & Definitions (21)

  • Example 1
  • Proposition 1
  • Lemma 1
  • Theorem 2
  • Theorem 3
  • Lemma 3
  • Example 4
  • Example 5
  • Example 6
  • Lemma 6
  • ...and 11 more