2020 · 19 citations · 17 references
ComputingComputer ScienceFormal MethodsKnowledge RepresentationNatural Language ProcessingPredicate LogicTemporal Knowledge RepresentationTemporal LogicDatalogLinear Temporal LogicMetric Temporal LogicPropositional ReasoningPropositional RepresentationPropositional Temporal LogicTemporal Logic ReasoningTemporal Operators
We study DatalogMTL—an extension of Datalog with metric temporal operators—under integer semantics, where the temporal domain of both interpretations and temporal operators consists of integer time points only. This is in contrast to the standard semantics, which is defined over the rational timeline. DatalogMTL under integer semantics is an interesting KR language: on the one hand, one can often assume the integer timeline in applications; on the other hand, it captures prominent temporal extensions of Datalog such as Datalog1S. We show that the choice of integer semantics leads to more favourable computational properties. We first show that reasoning over integers is at most as hard as reasoning over rationals for DatalogMTL and its natural fragments. Then, we investigate fragments of DatalogMTL where adopting the integer semantics makes reasoning easier. In particular, we show that complexity drops from P-hard to NC1-complete for the propositional fragment (where all object variables are grounded), and from TC0-hard to ACC0 for the linear fragment where the past diamond operator is the only metric operator allowed in rule bodies. Thus, reasoning in such fragments is both tractable and highly parallelisable, which suggests their appropriateness for data-intensive applications.
17
Specifying real-time properties with metric temporal logic
Ron Koymans · Real-Time Systems · 1990 · 1.2K citations
Ashok K. Chandra, Larry Stockmeyer, Uzi Vishkin · SIAM Journal on Computing · 1984 · 297 citations
Finite automata and unary languages
Marek Chrobák · Theoretical Computer Science · 1986 · 294 citations