Ontology-based data access (OBDA) augments classical query answering in databases by including domain knowledge provided by an ontology. An ontology captures the terminology of an application domain and describes domain knowledge in a machine-processable way. Formal ontology languages additionally provide semantics to these specifications. Systems for OBDA thus may apply logical reasoning to answer queries; they use the ontological knowledge to infer new information, which is only implicitly given in the data. Moreover, they usually employ the open-world assumption, which means that knowledge not stated explicitly in the data or inferred is neither assumed to be true nor false. Classical OBDA regards the knowledge however only w.r.t. a single moment, which means that information about time is not used for reasoning and hence lost; in particular, the queries generally cannot express temporal aspects. We investigate temporal query languages that allow to access temporal data through classical ontologies. In particular, we study the computational complexity of temporal query answering regarding ontologies written in lightweight description logics, which are known to allow for efficient reasoning in the atemporal setting and are successfully applied in practice. Furthermore, we present a so-called rewritability result for ontology-based temporal query answering, which suggests ways for implementation. Our results may thus guide the choice of a query language for temporal OBDA in data-intensive applications that require fast processing, such as context recognition.

Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerful logic that is equipped with a freeze formalism. It uses register variables, which can be set to the current data value and later these register variables can be compared with the current data value. For monotonic data words, Alur and Henzinger proved that MTL and TPTL are equally expressive and the satisfiability problem is decidable. We study the expressive power, satisfiability problems and path checking problems for MLT and TPTL over all data words. We introduce Ehrenfeucht-Fraisse games for MTL and TPTL. Using the EF-game for MTL, we show that TPTL is strictly more expressive than MTL. Furthermore, we show that the MTL definability problem that whether a TPTL-formula is definable in MTL is not decidable. When restricting the number of register variables, we are able to show that TPTL with two register variables is strictly more expressive than TPTL with one register variable. For the satisfiability problem, we show that for MTL, the unary fragment of MTL and the pure fragment of MTL, SAT is not decidable. We prove the undecidability by reductions from the recurrent state problem and halting problem of two-counter machines. For the positive fragments of MTL and TPTL, we show that a positive formula is satisfiable if and only it is satisfied by a finite data word. Finitary SAT and infinitary SAT coincide for positive MTL and positive TPTL. Both of them are r.e.-complete. For existential TPTL and existential MTL, we show that SAT is NP-complete. We also investigate the complexity of path checking problems for TPTL and MTL over data words. These data words can be either finite or infinite periodic. For periodic words without data values, the complexity of LTL model checking belongs to the class AC^1(LogDCFL). For finite monotonic data words, the same complexity bound has been shown for MTL by Bundala and Ouaknine. We show that path checking for TPTL is PSPACE-complete, and for MTL is P-complete. If the number of register variables allowed is restricted, we obtain path checking for TPTL with only one register variable is P-complete over both infinite and finite data words; for TPTL with two register variables is PSPACE-complete over infinite data words. If the encoding of constraint numbers of the input TPTL-formula is in unary notation, we show that path checking for TPTL with a constant number of variables is P-complete over infinite unary encoded data words. Since the infinite data word produced by a deterministic one-counter machine is periodic, we can transfer all complexity results for the infinite periodic case to model checking over deterministic one-counter machines.

Ontology-based data access (OBDA) augments classical query answering in databases by including domain knowledge provided by an ontology. An ontology captures the terminology of an application domain and describes domain knowledge in a machine-processable way. Formal ontology languages additionally provide semantics to these specifications. Systems for OBDA thus may apply logical reasoning to answer queries; they use the ontological knowledge to infer new information, which is only implicitly given in the data. Moreover, they usually employ the open-world assumption, which means that knowledge not stated explicitly in the data or inferred is neither assumed to be true nor false. Classical OBDA regards the knowledge however only w.r.t. a single moment, which means that information about time is not used for reasoning and hence lost; in particular, the queries generally cannot express temporal aspects. We investigate temporal query languages that allow to access temporal data through classical ontologies. In particular, we study the computational complexity of temporal query answering regarding ontologies written in lightweight description logics, which are known to allow for efficient reasoning in the atemporal setting and are successfully applied in practice. Furthermore, we present a so-called rewritability result for ontology-based temporal query answering, which suggests ways for implementation. Our results may thus guide the choice of a query language for temporal OBDA in data-intensive applications that require fast processing, such as context recognition.

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.

Often the addition of metric operators to qualitative temporal logics leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. The main result states that the language obtained by extending since/until logic of the real line with the operators 'sometime within n time units', n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.

Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerful logic that is equipped with a freeze formalism. It uses register variables, which can be set to the current data value and later these register variables can be compared with the current data value. For monotonic data words, Alur and Henzinger proved that MTL and TPTL are equally expressive and the satisfiability problem is decidable. We study the expressive power, satisfiability problems and path checking problems for MLT and TPTL over all data words. We introduce Ehrenfeucht-Fraisse games for MTL and TPTL. Using the EF-game for MTL, we show that TPTL is strictly more expressive than MTL. Furthermore, we show that the MTL definability problem that whether a TPTL-formula is definable in MTL is not decidable. When restricting the number of register variables, we are able to show that TPTL with two register variables is strictly more expressive than TPTL with one register variable. For the satisfiability problem, we show that for MTL, the unary fragment of MTL and the pure fragment of MTL, SAT is not decidable. We prove the undecidability by reductions from the recurrent state problem and halting problem of two-counter machines. For the positive fragments of MTL and TPTL, we show that a positive formula is satisfiable if and only it is satisfied by a finite data word. Finitary SAT and infinitary SAT coincide for positive MTL and positive TPTL. Both of them are r.e.-complete. For existential TPTL and existential MTL, we show that SAT is NP-complete. We also investigate the complexity of path checking problems for TPTL and MTL over data words. These data words can be either finite or infinite periodic. For periodic words without data values, the complexity of LTL model checking belongs to the class AC^1(LogDCFL). For finite monotonic data words, the same complexity bound has been shown for MTL by Bundala and Ouaknine. We show that path checking for TPTL is PSPACE-complete, and for MTL is P-complete. If the number of register variables allowed is restricted, we obtain path checking for TPTL with only one register variable is P-complete over both infinite and finite data words; for TPTL with two register variables is PSPACE-complete over infinite data words. If the encoding of constraint numbers of the input TPTL-formula is in unary notation, we show that path checking for TPTL with a constant number of variables is P-complete over infinite unary encoded data words. Since the infinite data word produced by a deterministic one-counter machine is periodic, we can transfer all complexity results for the infinite periodic case to model checking over deterministic one-counter machines.

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. Many real-world applications, like processing electronic health records (EHRs), also contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. Our contribution consists of three main parts: Firstly, we introduce a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic ELH⊥, which is based on the minimal universal model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity. Secondly, we introduce a new temporal variant of ELH⊥ that features a convexity operator. We extend this minimal-world semantics for answering metric temporal conjunctive queries with negation over the logic and obtain similar rewritability and complexity results. Thirdly, apart from the theoretical results, we evaluate minimal-world semantics in practice by selecting patients, based their EHRs, that match given criteria.

We present some initial results on ontology-based query answering with description logic ontologies that may employ temporal and probabilistic operators on concepts and axioms. Speci_cally, we consider description logics extended with operators from linear temporal logic (LTL), as well as subjective probability operators, and an extended query language in which conjunctive queries can be combined using these operators. We first show some complexity results for the setting in which either only temporal operators or only probabilistic operators may be used, both in the ontology and in the query, and then show a 2ExpSpace lower bound for the setting in which both types of operators can be used together. / This is an extended version of an article accepted at Description Logics 2019.

Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system’s behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any point in time yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to a trace satisfy (violate) the formula. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use the more expressive temporal logic ALC-LTL, which can use axioms of the Description Logic (DL) ALC instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behaviour provides us with complete information about the states of the system, we assume that states are described in an incomplete way by ALC-knowledge bases. We show that also in this setting monitors can effectively be constructed. The (double-exponential) size of the constructed monitors is in fact optimal, and not higher than in the propositional case. As an auxiliary result, we show how to construct Büchi automata for ALC-LTL-formulae, which yields alternative proofs for the known upper bounds of deciding satisfiability in ALC-LTL.

Es wird die Axiomatisierbarkeit einer Klasse von temporalen Prädikatenlogiken über verzweigenden Strukturen gezeigt. Entscheidbarkeitsresultate folgen für diverse Fragmente dieser Logiken. Anwendungen werden diskutiert.