Extremal Separation Problems for Temporal Instance Queries
Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev
TL;DR
This work studies extremal separation for temporal instance queries encoded in a fragment of Linear Temporal Logic (LTL) with operators $\land$, $\bigcirc$ and $\Diamond$. It introduces strengthening/weakening frontiers to succinctly represent the space of separating queries and derives a precise complexity landscape, showing containment in $\mathsf{P}$ for many classes (notably $\mathcal{Q}_p[\Diamond]$ and path variants) while proving $\mathsf{co}$NP-completeness for unique most-specific separators in several cases and $\#\mathsf{P}$-hardness for counting separators. The authors provide graph-based algorithms that encode example sets and compute longest/shortest, unique, or general separators in time $O(t_+^{c_+} t_-^{c_-})$, enabling practical synthesis of explanations via temporal patterns. The results bridge logic, automata, and pattern-matching perspectives, yielding both theoretical and algorithmic insights into query-by-example for temporal data and highlighting open problems for broader temporal languages.
Abstract
The separation problem for a class Q of database queries is to find a query in Q that distinguishes between a given set of `positive' and `negative' data examples. Separation provides explanations of examples and underpins the query-by-example paradigm to support database users in constructing and refining queries. As the space of all separating queries can be large, it is helpful to succinctly represent this space by means of its most specific (logically strongest) and general (weakest) members. We investigate this extremal separation problem for classes of instance queries formulated in linear temporal logic LTL with the operators conjunction, next, and eventually. Our results range from tight complexity bounds for verifying and counting extremal separators to algorithms computing them.