Deciding FO-rewritability of Ontology-Mediated Queries in Linear Temporal Logic

Aiming at ontology-based data access to temporal data, we investigate the problems of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL and deciding whether it is rewritable to an FO(<)-formula, possibly with extra built-in predicates. Using known facts about the complexity of regular languages, we show that OMQ answering in AC0 coincides with FO(<,≡N)-rewritiability, which admits unary predicates x ≡ 0(mod n), and that deciding FO(<)- and FO(<,≡N)-rewritiability of LTL OMQs is ExpSpace-complete. We further observe that answering any OMQ is either in ACC0, in which case it is FO(<,MOD)-rewritable, or NC1complete, and prove that distinguishing between these two cases can be done in ExpSpace. Finally, we identify fragments of LTL for which some of these decision problems become PSpace-, Πp 2- and coNP-complete.