Vlad Ryzhikov

On Horn fragments of Metric Temporal Logic

Metric Temporal Logic (MTL) has recently been shown to be a well-suited formalism for describing events observable in temporal log data supplied, for instance, by sensors. Dense linear orders are used as a model of time in this scenario, since it does not make sense to assume periodicity or minimal unit of time for sensor outputs. We study the problem of ontology-mediated query answering (OMQA), where the ontology is given as a set of universal MTL clauses, and the query is an event name (atom) mentioned in it. Satisfiability and, therefore, OMQA in MTL over dense time is known to be undecidable. We show that restricting MTL clauses to the Horn shape leads to ExpTime-complete reasoning without hurting the expressivity for the considered applications. We then consider several other related syntactic restrictions on the shape of the clauses and their effect on complexity.