Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is a linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly monotonic integer-time semantics. MTL has been described as a prominent specification formalism for real-time systems. Full MTL over infinite timed words is undecidable.
Syntax The full metric temporal logic is defined similarly to linear temporal logic, where a set of non-negative real numbers is added to temporal modal operators U and S. Formally, MTL is built up from:
a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operator UI (pronounced "φ until in I ψ."), with I an interval of non-negative numbers. the temporal modal operator SI (pronounced "φ since in I ψ."), with I as above. When the subscript is omitted, it is implicitly equal to [ 0 , ∞ ) {\displaystyle [0,\infty )} . Note that the next operator N is not considered to be a part of MTL syntax. It will instead be defined from other operators.
Past and Future The past fragment of metric temporal logic, denoted as past-MTL is defined as the restriction of the full metric temporal logic without the until operator. Similarly, the future fragment of metric temporal logic, denoted as future-MTL is defined as the restriction of the full metric temporal logic without the since operator. Depending on the authors, MTL is either defined as the future fragment of MTL, in which case full-MTL is called MTL+Past. Or MTL is defined as full-MTL. In order to avoid ambiguity, this article uses the names full-MTL, past-MTL and future-MTL. When the statements holds for the three logic, MTL will simply be used.
Model Let T ⊆ R + {\displaystyle T\subseteq \mathbb {R} _{+}} intuitively represent a set of points in time. Let γ : T → A {\displaystyle \gamma :T\to A} a function which associates a letter to each moment t ∈ T {\displaystyle t\in T} . A model of a MTL formula is such a function γ {\displaystyle \gamma } . Usually, γ {\displaystyle \gamma } is either a timed word or a signal. In those cases, T {\displaystyle T} is either a discrete subset or an interval containing 0.
Semantics Let T {\displaystyle T} and γ {\displaystyle \gamma } as above and let t ∈ T {\displaystyle t\in T} some fixed time. We are now going to explain what it means that a MTL formula ϕ {\displaystyle \phi } holds at time t {\displaystyle t} , which is denoted γ , t ⊨ ϕ {\displaystyle \gamma ,t\models \phi } . Let I ⊆ R + {\displaystyle I\subseteq \mathbb {R} _{+}} and ϕ , ψ ∈ M T L {\displaystyle \phi ,\psi \in MTL} . We first consider the formula ϕ U I ψ {\displaystyle \phi {\mathcal {U}}_{I}\psi } . We say that γ , t ⊨ ϕ U I ψ {\displaystyle \gamma ,t\models \phi {\mathcal {U}}_{I}\psi } if and only if there exists some time t ′ ∈ t + I {\displaystyle t'\in t+I} such that:
γ , t ′ ⊨ ψ {\displaystyle \gamma ,t'\models \psi } and for each t ″ ∈ T {\displaystyle t''\in T} with t < t ″ < t ′ {\displaystyle t<t''<t'} , γ , t ″ ⊨ ϕ {\displaystyle \gamma ,t''\models \phi } . We now consider the formula ϕ S I ψ {\displaystyle \phi {\mathcal {S}}_{I}\psi } (pronounced " ϕ {\displaystyle \phi } since in I {\displaystyle I} ψ {\displaystyle \psi } .") We say that γ , t ⊨ ϕ S I ψ {\displaystyle \gamma ,t\models \phi {\mathcal {S}}_{I}\psi } if and only if there exists some time t ′ ∈ t − I {\displaystyle t'\in t-I} such that:
… excerpt ends here. Continue reading the full article.
