Overview
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 (pronounced " until in ."), with an interval of non-negative numbers. * the temporal modal operator (pronounced " since in ."), with as above. When the subscript is omitted, it is implicitly equal to 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\subseteq\mathbb R_+ intuitively represent a set of points in time. Let \gamma: T\to A a function which associates a letter to each moment t\in T . A model of a MTL formula is such a function \gamma . Usually, \gamma is either a timed word or a signal. In those cases, T is either a discrete subset or an interval containing 0.
Semantics
Let T and \gamma as above and let t\in T some fixed time. We are now going to explain what it means that a MTL formula \phi holds at time t , which is denoted \gamma,t\models\phi . Let I\subseteq\mathbb R_+ and \phi,\psi\in MTL . We first consider the formula \phi\mathcal U_I\psi . We say that \gamma,t\models\phi\mathcal U_I\psi if and only if there exists some time t'\in t+I such that: * \gamma,t'\models\psi and * for each t\in T with t , \gamma,t\models\phi . We now consider the formula \phi\mathcal S_I\psi (pronounced " \phi since in I \psi .") We say that \gamma,t\models\phi\mathcal S_I\psi if and only if there exists some time t'\in t-I such that: * \gamma,t'\models\psi and * for each t\in T with t' , \gamma,t\models\phi . The definitions of \gamma,t\models\phi for the values of \phi not considered above is similar as the definition in the LTL case.
Operators defined from basic MTL operators
Some formulas are so often used that a new operator is introduced for them. These operators are usually not considered to belong to the definition of MTL, but are syntactic sugar which denote more complex MTL formula. We first consider operators which also exists in LTL. In this section, we fix \phi,\psi MTL formulas and I\subseteq\mathbb R_+ .
Release and Back to
We denote by \phi\mathcal R_I\psi (pronounced " \phi release in I , \psi ") the formula \neg(\neg\phi\mathcal U_I\neg\psi) . This formula holds at time t if either: * there is some time t'\in t+I such that \phi holds, and \psi hold in the interval (t,t')\cap (t+I) . * at each time t'\in t+I , \psi holds. The name "release" come from the LTL case, where this formula simply means that \psi should always hold, unless \phi releases it. The past counterpart of release is denote by \phi\mathcal B_I\psi (pronounced " \phi back to in I , \psi ") and is equal to the formula \neg(\neg\phi\mathcal S_I\neg\psi) .
Finally and Eventually
We denote by \Diamond_I\phi or \mathcal F_I\phi (pronounced "Finally in I , \phi ", or "Eventually in I , \phi ") the formula \top\mathcal U_I\phi . Intuitively, this formula holds at time t if there is some time t'\in t+I such that \phi holds. We denote by \Box_I\phi or \mathcal G_I\phi (pronounced "Globally in I , \phi ",) the formula \neg\Diamond_I\neg\phi . Intuitively, this formula holds at time t if for all time t'\in t+I , \phi holds. We denote by \overleftarrow\Box_I\phi and \overleftarrow\Diamond_I\phi the formula similar to \Box_I\phi and \Diamond_I\phi , where \mathcal U is replaced by \mathcal S . Both formula has intuitively the same meaning, but when we consider the past instead of the future.
Next and previous
This case is slightly different from the previous ones, because the intuitive meaning of the "Next" and "Previously" formulas differs depending on the kind of function \gamma considered. We denote by \bigcirc_I\phi or \mathcal N_I\phi (pronounced "Next in I , \phi ") the formula \bot\mathcal U_I\phi . Similarly, we denote by \ominus_I\phi (pronounced "Previously in I , \phi ) the formula \bot\mathcal S_I\phi . The following discussion about the Next operator also holds for the Previously operator, by reversing the past and the future.
When this formula is evaluated over a timed word \gamma:T\to A , this formula means that both: * at the next time in the domain of definition T , the formula \phi will holds. * furthermore, the distance between this next time and the current time belong to the interval I . * In particular, this next time holds, thus the current time is not the end of the word. When this formula is evaluated over a signal \gamma , the notion of next time does not makes sense. Instead, "next" means "immediately after". More precisely \gamma,t\models\circ\phi means: * I contains an interval of the form (0,\epsilon) and * for each t'\in(t,t+\epsilon) , \gamma,t'\models\phi .
Other operators
We now consider operators which are not similar to any standard LTL operators.
Fall and Rise
We denote by \uparrow\phi (pronounced "rise \phi "), a formula which holds when \phi becomes true. More precisely, either \phi did not hold in the immediate past, and holds at this time, or it does not hold and it holds in the immediate future. Formally \uparrow\phi is defined as (\phi\land(\neg\phi\mathcal S\top))\lor(\neg\phi\land(\phi\mathcal U\top)) . Over timed words, this formula always hold. Indeed \phi\mathcal U\top and \neg\phi\mathcal S\top always hold. Thus the formula is equivalent to \phi\lor\neg\phi , hence is true. By symmetry, we denote by \downarrow\phi (pronounced "Fall \phi ), a formula which holds when \phi becomes false. Thus, it is defined as (\neg\phi\land(\phi\mathcal S\top))\land(\phi\land(\neg\phi\mathcal U\top)) .
History and Prophecy
We now introduce the prophecy operator, denoted by \triangleright . We denote by \triangleright_I\phi the formula \neg\phi\mathcal U_I\phi . This formula asserts that there exists a first moment in the future such that \phi holds, and the time to wait for this first moment belongs to I . We now consider this formula over timed words and over signals. We consider timed words first. Assume that I=\mid a,b\mid' where \mid and \mid' represents either open or closed bounds. Let \gamma a timed word and t in its domain of definition. Over timed words, the formula \gamma,t\models\triangleright_I\phi holds if and only if \gamma,t\models\Box_ 0,b \setminus I \neg\phi\land\Diamond_I\phi also holds. That is, this formula simply assert that, in the future, until the interval t+I is met, \phi should not hold. Furthermore, \phi should hold sometime in the interval t+I .
Indeed, given any time t\in t+I such that \gamma,t\models\phi hold, there exists only a finite number of time t'\in t+I with t' and \gamma,t'\models\phi . Thus, there exists necessarily a smaller such t . Let us now consider signal. The equivalence mentioned above does not hold anymore over signal. This is due to the fact that, using the variables introduced above, there may exists an infinite number of correct values for t' , due to the fact that the domain of definition of a signal is continuous. Thus, the formula \triangleright_I\phi also ensures that the first interval in which \phi holds is closed on the left. By temporal symmetry, we define the history operator, denoted by \triangleleft . We define \triangleleft_I\phi as \neg\phi\mathcal S_I\phi . This formula asserts that there exists a last moment in the past such that \phi held.
And the time since this first moment belongs to I .
Non-strict operator
The semantic of operators until and since introduced do not consider the current time. That is, in order for \phi_1\mathcal U \phi_2 to holds at some time t , neither \phi_1 nor \phi_2 has to hold at time t . This is not always wanted, for example in the sentence "there is no bug until the system is turned-off", it may actually be wanted that there are no bug at current time. Thus, we introduce another until operator, called non-strict until, denoted by \overline \mathcal U , which consider the current time. We denote by \phi_1\overline \mathcal U _ I \phi_2 and \phi_1\overline \mathcal S _ I \phi_2 either: * the formulas \phi_2\lor(\phi_1\land (\phi_1\mathcal U_ I \phi_2)) and \phi_2\lor(\phi_1\land (\phi_1\mathcal S_ I \phi_2)) if 0\in I , and * the formulas \phi_1\land(\phi_1\mathcal U_ I \phi_2) and \phi_1\land(\phi_1\mathcal S_ I \phi_2) otherwise.
For any of the operators \mathcal O introduced above, we denote \overline \mathcal O the formula in which non-strict untils and sinces are used. For example \overline\Diamond p is an abbreviation for \top\overline \mathcal U p . Strict operator can not be defined using non-strict operator. That is, there is no formula equivalent to \bigcirc_I p which uses only non-strict operator. This formula is defined as \bot\mathcal U_I p . This formula can never hold at a time t if it is required that \bot holds at time t .
Example
We now give examples of MTL formulas. Some more example can be found on article of fragments of MITL, such as metric interval temporal logic. * \Box(p\implies\Diamond_ \ 1\ q) states that each letter p is followed exactly one time unit later by a letter q . * \Box(p\implies\neg\Diamond_ \ 1\ p) states that no two successive occurrences of p can occur at exactly one time unit from each other.
Comparison with LTL
A standard (untimed) infinite word w=a_0,a_1,\dots, is a function from \mathbb N to A . We can consider such a word using the set of time T=\mathbb N , and the function \gamma(i)=a_i . In this case, for \phi an arbitrary LTL formula, w,i\models\phi if and only if \gamma,i\models\phi , where \phi is considered as a MTL formula with non-strict operator and 0,\infty) subscript. In this sense, MTL is an extension of LTL. For this reason, a formula using only non-strict operator with 0,\infty) subscript is called an LTL formula.
Algorithmic complexity
The satisfiability of ECL over signals is EXPSPACE-complete.
Fragments of MTL
We now consider some fragments of MTL.
MITL
An important subset of MTL is the Metric Interval Temporal Logic (MITL). This is defined similarly to MTL, with the restriction that the sets I , used in \mathcal U and \mathcal S , are intervals which are not singletons, and whose bounds are natural numbers or infinity. Some other subsets of MITL are defined in the article MITL.
Future Fragments
Future-MTL was already introduced above. Both over timed-words and over signals, it is less expressive than Full-MTL.
Event-Clock Temporal Logic
The fragment Event-Clock Temporal Logic of MTL, denoted EventClockTL or ECL, allows only the following operators: * the boolean operators, and, or, not * the untimed until and since operators. * The timed prophecy and history operators. Over signals, ECL is as expressive as MITL and as MITL 0 . The equivalence between the two last logics is explained in the article MITL 0 . We sketch the equivalence of those logics with ECL. If I is not a singleton and \phi is a MITL formula, \triangleright_I\phi is defined as a MITL formula. If I=\ i\ is a singleton, then \triangleright_I\phi is equivalent to \Box_ 0,i \neg\phi\land\Diamond_ 0,i \phi which is a MITL-formula. Reciprocally, for \psi an ECL-formula, and I an interval whose lower bound is 0, \Box_I\psi is equivalent to the ECL-formula \neg\triangleright_I\neg\psi . The satisfiability of ECL over signals is PSPACE-complete.
Positive normal form
A MTL-formula in positive normal form is defined almost as any MTL formula, with the two following change: * the operators Release and Back are introduced in the logical language and are not considered anymore to be notations for some other formulas. * negations can only be applied to letters. Any MTL formula is equivalent to formula in normal form. This can be shown by an easy induction on formulas. For example, the formula \neg(\phi\mathcal U_ S \psi) is equivalent to the formula (\neg\phi)\mathcal R_ S (\neg\psi) . Similarly, conjunctions and disjunctions can be considered using De Morgan's laws. Strictly speaking, the set of formulas in positive normal form is not a fragment of MTL.
See also
* Timed propositional temporal logic, another extension of LTL in which time can be measured.