arXiv subjects

Vladislav Ryzhikov

Publications and source records attributed to Vladislav Ryzhikov.

At least 19 recordsLinked to original sources

arXiv2025

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

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

cs.AI↗

arXiv2024

Unique Characterisability and Learnability of Temporal Queries Mediated by an Ontology

Algorithms for learning database queries from examples and unique characterisations of queries by examples are prominent starting points for developing automated support for query construction and explanation. We investigate how far recent results and techniques on learning and unique characterisations of atemporal queries mediated by an ontology can be extended to temporal data and queries. Based on a systematic review of the relevant approaches in the atemporal case, we obtain general transfer results identifying conditions under which temporal queries composed of atemporal ones are (polynomially) learnable and uniquely characterisable.

cs.AI↗

arXiv2024

Extremal Separation Problems for Temporal Instance Queries

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.

cs.DB↗

arXiv2023

Reverse Engineering of Temporal Queries Mediated by LTL Ontologies

In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explanation of the answers and non-answers. We investigate this query-by-example problem for queries formulated in positive fragments of linear temporal logic LTL over timestamped data, focusing on the design of suitable query languages and the combined and data complexity of deciding whether there exists a query in the given language that separates the given answers from non-answers. We consider both plain LTL queries and those mediated by LTL-ontologies.

cs.LO↗

arXiv2023

Deciding FO-rewritability of regular languages and ontology-mediated queries in Linear Temporal Logic

Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) formulated in linear temporal logic LTL over (Z,<) and deciding whether it is rewritable to an FO(<)-query, possibly with some extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC^0, ACC^0 and NC^1 coincides with FO(<,\equiv)-rewritability using unary predicates x \equiv 0 (mod n), FO(<,MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of regular languages, deciding FO(<,\equiv)- and FO(<,MOD)-definability is also \PSPACE-complete (unless ACC^0 = NC^1). We then use this result to show that deciding FO(<)-, FO(<,\equiv)- and FO(<,MOD)-rewritability of LTL OMQs is EXPSPACE-complete, and that these problems become PSPACE-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<,\equiv)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSPACE-, Pi_2^p- and coNP-complete.

cs.CC↗

arXiv2022

First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries

Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z,<). Our main concern is first-order rewritability of ontology-mediated queries (OMQs) that consist of a 2D ontology and a positive temporal instance query. Our target languages for FO-rewritings are two-sorted FO(<) - first-order logic with sorts for time instants ordered by the built-in precedence relation < and for the domain of individuals - its extension FOE with the standard congruence predicates t \equiv 0 mod n, for any fixed n > 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FOE- and FO(RPR)-rewritability guarantee answering OMQs in uniform AC0 and NC1, respectively. We proceed in three steps. First, we define a hierarchy of 2D DL-Lite/LTL ontology languages and investigate the FO-rewritability of OMQs with atomic queries by constructing projections onto 1D LTL OMQs and employing recent results on the FO-rewritability of propositional LTL OMQs. As the projections involve deciding consistency of ontologies and data, we also consider the consistency problem for our languages. While the undecidability of consistency for 2D ontology languages with expressive Boolean role inclusions might be expected, we also show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to decidability (and ExpSpace-completeness), even if one admits full Booleans on concepts. As a final step, we lift some of the rewritability results for atomic OMQs to OMQs with expressive positive temporal instance queries. The lifting results are based on an in-depth study of the canonical models and only concern Horn ontologies.

cs.LO↗

arXiv2022

Unique Characterisability and Learnability of Temporal Instance Queries

We aim to determine which temporal instance queries can be uniquely characterised by a (polynomial-size) set of positive and negative temporal data examples. We start by considering queries formulated in fragments of propositional linear temporal logic LTL that correspond to conjunctive queries (CQs) or extensions thereof induced by the until operator. Not all of these queries admit polynomial characterisations but by restricting them further to path-shaped queries we identify natural classes that do. We then investigate how far the obtained characterisations can be lifted to temporal knowledge graphs queried by 2D languages combining LTL with concepts in description logics EL or ELI (i.e., tree-shaped CQs). While temporal operators in the scope of description logic constructors can destroy polynomial characterisability, we obtain general transfer results for the case when description logic constructors are within the scope of temporal operators. Finally, we apply our characterisations to establish (polynomial) learnability of temporal instance queries using membership queries in the active learning framework.

cs.LO↗

arXiv2021

Deciding FO-definability of regular languages

We prove that, similarly to known PSpace-completeness of recognising FO(<)-definability of the language L(A) of a DFA A, deciding both FO(<,C)- and FO(<,MOD)-definability are PSpace-complete. (Here, FO(<,C) extends the first-order logic FO(<) with the standard congruence modulo n relation, and FO(<,MOD) with the quantifiers checking whether the number of positions satisfying a given formula is divisible by a given n>1. These FO-languages are known to define regular languages that are decidable in AC0 and ACC0, respectively.) We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by `localisable' properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSpace-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for two-way NFAs.

cs.LO↗

arXiv2021

First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic

We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time (Z,<). Queries are given in LTL or MFO(<), monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account of the temporal operators used in the ontology and distinguishing between ontologies given in full LTL and its core, Krom and Horn fragments, we identify a hierarchy of OMQs with atomic queries by proving rewritability into either FO(<), first-order logic with the built-in linear order, or FO(<,E), which extends FO(<) with the standard arithmetic predicates saying that "x is equivalent to 0 modulo n", for any fixed n > 1, or FO(RPR), which extends FO(<) with relational primitive recursion. In terms of circuit complexity, FO(<,E)- and FO(RPR)-rewritability guarantee OMQ answering in uniform AC0 and, respectively, NC1. We obtain similar hierarchies for more expressive types of queries: positive LTL-formulas, monotone MFO(<)- and arbitrary MFO(<)-formulas. Our results are directly applicable if the temporal data to be accessed is one-dimensional; moreover, they lay foundations for investigating ontology-based access using combinations of temporal and description logics over two-dimensional temporal data.

cs.LO↗

arXiv2020

The Complexity of Ontology-Based Data Access with OWL 2 QL and Bounded Treewidth Queries

Our concern is the overhead of answering OWL 2 QL ontology-mediated queries (OMQs) in ontology-based data access compared to evaluating their underlying tree-shaped and bounded treewidth conjunctive queries (CQs). We show that OMQs with bounded-depth ontologies have nonrecursive datalog (NDL) rewritings that can be constructed and evaluated in LOGCFL for combined complexity, even in NL if their CQs are tree-shaped with a bounded number of leaves, and so incur no overhead in complexity-theoretic terms. For OMQs with arbitrary ontologies and bounded-leaf CQs, NDL-rewritings are constructed and evaluated in LOGCFL. We show experimentally feasibility and scalability of our rewritings compared to previously proposed NDL-rewritings. On the negative side, we prove that answering OMQs with tree-shaped CQs is not fixed-parameter tractable if the ontology depth or the number of leaves in the CQs is regarded as the parameter, and that answering OMQs with a fixed ontology (of infinite depth) is NP-complete for tree-shaped and LOGCFL for bounded-leaf CQs.

cs.DB↗

arXiv2019

Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)

We investigate the data complexity of answering queries mediated by metric temporal logic ontologies under the event-based semantics assuming that data instances are finite timed words timestamped with binary fractions. We identify classes of ontology-mediated queries answering which can be done in AC0, NC1, L, NL, P, and coNP for data complexity, provide their rewritings to first-order logic and its extensions with primitive recursion, transitive closure or datalog, and establish lower complexity bounds.

cs.LO↗

arXiv2019

Query Inseparability for ALC Ontologies

We investigate the problem whether two ALC ontologies are indistinguishable (or inseparable) by means of queries in a given signature, which is fundamental for ontology engineering tasks such as ontology versioning, modularisation, update, and forgetting. We consider both knowledge base (KB) and TBox inseparability. For KBs, we give model-theoretic criteria in terms of (finite partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs), but 2ExpTime-complete for unions of CQs (UCQs). The same results hold if (U)CQs are replaced by rooted (U)CQs, where every variable is connected to an answer variable. We also show that inseparability by CQs is still undecidable if one KB is given in the lightweight DL EL and if no restrictions are imposed on the signature of the CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query over any ABox in a given signature and show that, for CQs, this problem is undecidable, too. We then develop model-theoretic criteria for Horn-ALC TBoxes and show using tree automata that, in contrast, inseparability becomes decidable and 2ExpTime-complete, even ExpTime-complete when restricted to (unions of) rooted CQs.

cs.AI↗

arXiv2018

Querying Log Data with Metric Temporal Logic (Technical Report)

We propose a novel framework for ontology-based access to temporal log data using a datalog extension datalogMTL of a Horn fragment of the metric temporal logic MTL. We show that datalogMTL is ExpSpace-complete even with punctual intervals, in which case full MTL is known to be undecidable. We also prove that nonrecursive datalogMTL is PSpace-complete for combined complexity and in AC0 for data complexity. We demonstrate by two real-world use cases that nonrecursive datalogMTL programs can express complex temporal concepts from typical user queries and thereby facilitate access to temporal log data. Our experiments with Siemens turbine data and MesoWest weather data show that datalogMTL ontology-mediated queries are efficient and scale on large datasets.

cs.LO↗

arXiv2018

Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey

The question whether an ontology can safely be replaced by another, possibly simpler, one is fundamental for many ontology engineering and maintenance tasks. It underpins, for example, ontology versioning, ontology modularization, forgetting, and knowledge exchange. What safe replacement means depends on the intended application of the ontology. If, for example, it is used to query data, then the answers to any relevant ontology-mediated query should be the same over any relevant data set; if, in contrast, the ontology is used for conceptual reasoning, then the entailed subsumptions between concept expressions should coincide. This gives rise to different notions of ontology inseparability such as query inseparability and concept inseparability, which generalize corresponding notions of conservative extensions. We survey results on various notions of inseparability in the context of description logic ontologies, discussing their applications, useful model-theoretic characterizations, algorithms for determining whether two ontologies are inseparable (and, sometimes, for computing the difference between them if they are not), and the computational complexity of this problem.

cs.AI↗

arXiv2017

Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics, but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.

cs.LO↗

arXiv2017

Metric Temporal Logic for Ontology-Based Data Access over Log Data

We present a new metric temporal logic HornMTL over dense time and its datalog extension datalogMTL. The use of datalogMTL is demonstrated in the context of ontology-based data access over meteorological data. We show decidability of answering ontology-mediated queries for a practically relevant non-recursive fragment of datalogMTL. Finally, we discuss directions of the future work, including the potential use-cases in analyzing log data of engines and devices.

cs.LO↗

arXiv2016

Query-Based Entailment and Inseparability for ALC Ontologies (Full Version)

We investigate the problem whether two ALC knowledge bases are indistinguishable by queries over a given vocabulary. We give model-theoretic criteria in terms of (partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs) but 2EXPTIME-complete for UCQs (unions of CQs). The same results hold if CQs are replaced by rooted CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query in a given vocabulary over all ABoxes, and show that for CQs this problem is undecidable, too, but becomes decidable and 2EXPTIME-complete in Horn-ALC, and even EXPTIME-complete in Horn-ALC when restricted to (unions of) rooted CQs.

cs.LO↗

arXiv2014

A Cookbook for Temporal Conceptual Data Modelling with Description Logics

We design temporal description logics suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based on DL-Lite logics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. In the temporal dimension, they capture future and past temporal operators on concepts, flexible and rigid roles, the operators `always' and `some time' on roles, data assertions for particular moments of time and global concept inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (Z,<), satisfying the constant domain assumption. We prove that the most expressive of our temporal description logics (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turn out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions we obtain logics whose complexity ranges between PSpace and NLogSpace. These positive results were obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.

cs.LO↗