Motivation Context-aware systems use data collected at runtime to recognize predefined situations and trigger adaptations; e.g., an operating system may use sensors to recognize that a video application is out of user focus, and then adapt application parameters to optimize the energy consumption. Using ontologybased data access [12, 19], the situations can be encoded into queries that are answered over an ABox containing the sensor data. In the TBox, we can encode background knowledge about the domain. For example, if the user has been working with another application on a second screen for a longer period, then we may assume that he does not need the video to be displayed in the highest resolution. In this paper, we focus on the lightweight DL EL. We can state static knowledge about applications (VideoApplication(app1)), dynamic knowledge about the current context (NotWatchingVideo(user1)), as well as background knowledge like VideoApplication u 9hasUser:NotWatchingVideo v 9hasState:OutOfFocus; saying that a video application whose user is currently not watching the video is out of user focus. Given such a knowledge base, we can use the conjunctive query (CQ) (x) := 9y:hasState(x; y) ^ OutOfFocus(y) to identify applications x that can potentially be assigned a lower priority. More complex situations typically depend also on the behavior of the environment in the past-the operating system should not switch configurations every time the user is not watching for one second, but only after this has been the case for a longer period. For that reason, we investigate temporal conjunctive queries (TCQs), originally proposed in [3, 4]. They combine conjunctive queries via the operators of the propositional linear temporal logic LTL [14, 18]. We can use the TCQ
to obtain all applications that were out of user focus during the three previous (# ) moments of observation, were prioritized by the operating system at some point in time, and the priority has not (:) changed since (S) then. The semantics of TCQs is based on temporal knowledge bases (TKBs), which, in addition to the TBox (which is assumed to hold globally, i.e., at every point in time), contains a sequence of ABoxes A0; A1; : : : ; An, representing the data collected at specific
Partially supported by the DFG in CRC 912 (HAEC). points in time. We designate with n the most recent time of observation (the current time point ), at which the situation recognition is performed. We also investigate the related temporalized formalism EL-LTL, in which axioms, i.e., assertions or GCIs, are combined using LTL-operators.
Related Work The axioms in a TKB do not explicitly refer to time, but are
written in a classical (atemporal) DL; only the query is temporalized. In contrast,
[
Regarding temporal properties formulated over atemporal DLs, ALC-LTL,
a variant of EL-LTL over the more expressive DL ALC, was first considered
in [
Results We investigate the combined and data complexity of the TCQ
entailment problem over TKBs formulated in EL. Moreover, we determine the
complexity of satisfiability of EL-LTL-formulae, and additionally consider the
special case where only global GCIs are allowed [
With a single exception, the complexity of TCQ entailment in EL turns out to
be lower than that in ALC (and SHQ) [
The upper bounds are obtained by a combination of techniques that were
developed for ALC-LTL [
Individually, the satisfiability of the conjunctions i can be tested in P w.r.t. data complexity and in PSpace w.r.t. combined complexity. However, the problem is to ensure the first condition, namely that all rigid names are interpreted in the same way by all relevant interpretations.
In case (i), this restriction is obviously irrelevant. For case (iii), one can answer an exponentially large UCQ over an exponentially large atemporal knowledge base instead to obtain the upper bounds. The most difficult cases were case (ii) for the combined complexity of TCQ entailment, and the case of global GCIs in EL-LTL, where we needed to obtain PSpace upper bounds in the presence of rigid names. For these cases, we proved that it suffices to guess additional data of polynomial size that can be added to the knowledge bases in order to separate the satisfiability tests in Definition 1. These tests can then be integrated into a PSpace-Turing machine for LTL-satisfiability [20] without increasing the complexity.
Acknowledgements We want to thank Franz Baader, Marcel Lippmann, and Carsten Lutz for fruitful discussions on the topic of this paper. 1 In the case of EL-LTL, these are axioms. 17. Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey.
In: Proc. of the 15th Int. Symp. on Temporal Representation and Reasoning (TIME’08). pp. 3–14. IEEE Press (2008) 18. Pnueli, A.: The temporal logic of programs. In: Proc. of the 18th Annual Symp.
on Foundations of Computer Science (SFCS’77). pp. 46–57. IEEE Press (1977) 19. Poggi, A., Lembo, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.:
Linking data to ontologies. Journal of Data Semantics 10, 133–173 (2008) 20. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics.
Journal of the ACM 32(3), 733–749 (1985) 21. Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. of the 24th Annual Symp. on Foundations of Computer Science (SFCS’83). pp. 185–194. IEEE Press (1983)