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.
翻译:对于数据库查询类Q,分离问题是指在Q中寻找一个查询,能够区分给定的“正例”和“反例”数据样例集。分离提供了样例的解释,并支持“以样例查询”范式,帮助数据库用户构建和优化查询。由于所有分离查询的空间可能很大,通过其最特定(逻辑最强)和最一般(逻辑最弱)成员来简洁表示该空间是很有帮助的。我们研究了在线性时态逻辑LTL(包含合取、next和eventually算子)中实例查询类的极值分离问题。我们的结果涵盖了从验证和计数极值分离器的严格复杂度界限到计算这些分离器的算法。