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(＜, ≡), which extends FO(＜) with the standard arithmetic predicates x ≡ 0(mod n), for any fixed n ＞ 1, or FO(RPR), which extends FO(＜) with relational primitive recursion. In terms of circuit complexity, FO(＜,≡)- and FO(RPR)-rewritability guarantee OMQ answering in uniform AC~0 and, respectively, NC~1. 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.