On Syntactical Simplification of Temporal Operators in Negation-free MTL

Abstract

Temporal reasoning in dynamic, data-intensive environments increasingly demands expressive yet tractable logical frameworks. Traditional approaches often rely on negation to express absence or contradiction. In such contexts, Negation-as-Failure is commonly used to infer negative information from the lack of positive evidence. However, open and distributed systems such as IoT networks or the Semantic Web Negation-as-Failure semantics become unreliable due to incomplete and asynchronous data. This has led to a growing interest in negation-free fragments of temporal rule-based systems, which preserve monotonicity and enable scalable reasoning. This paper investigates the expressive power of negation-free MTL, a temporal logic framework designed for rule-based reasoning over time. We show that the "always" operators of MTL, often treated as syntactic sugar for combinations of other temporal constructs, can be eliminated using "once", "since" and "until" operators. Remarkably, even the "once" operators can be removed, yielding a fragment based solely on "until" and "since". These results challenge the assumption that negation is necessary for expressing universal temporal constraints, and reveal a robust fragment capable of capturing both existential and invariant temporal patterns. Furthermore, the results induce a reduction in the syntax of MTL, which in turn can provide benefits for both theoretical study as well as implementation efforts.