Metric interval temporal logic

A MITL formula is an MTL formula, such that each set of reals used in subscript are intervals, which are not singletons, and whose bounds are either a natural number or are infinite.{{Citation needed|date=September 2021}}

MTL can express a statement such as the sentence S: "P held exactly ten time units ago". This is impossible in MITL. Instead, MITL can say T: "P held between 9 and 10 time units ago". Since MITL can express T but not S, in a sense, MITL is a restriction of MTL which allows only less precise statements.

One reason to want to avoid a statement such as S is that its truth value may change an arbitrary number of times in a single time unit. Indeed, the truth value of this statement may change as many times as the truth value of P changes, and P itself may change an arbitrary number of time in a single time unit.

Let us now consider a system, such as a timed automaton or a signal automaton, which want to know at each instant whether S holds or not. This system should recall everything that occurred in the last 10 time units. As seen above, it means that it must recall an arbitrarily large number of events. This can not be implemented by a system with finite memory and clocks.

One of the main advantage of MITL is that each operator has the bounded variability property. Example:

Given the statement T defined above. Each time the truth value of T switches from false to true, it remains true for at least one time unit. Proof: At a time t where T becomes true, it means that:

• between 9 and 10 time units ago, P was true.
• just before time t, P was false.

Hence, P was true exactly 9 time units ago. It follows that, for each $t\text{'}\backslash in[0,1]$, at time $t+t\text{'}$, P was true $9+t\text{'}$ time units ago. Since $9+t\text{'}\backslash in[9,10]$, at time $t\text{'}$, T holds.

A system, at each instant, wants to know the value of T. Such a system must recall what occurred during the last ten time units. However, thanks to the bounded variability property, it must recall at most 10 time units when T becomes true. And hence 11 times when T becomes false. Thus this system must recall at most 21 events, and hence can be implemented as a timed automaton or a signal automaton.

Examples of MITL formulas:

• $\backslash square\backslash diamond\_\{(0,1)\}p$ states that the letter $p$ appears at least once in each open interval of length 1.
• $\backslash triangleright\_\{\backslash \{i\backslash \}\}p$ where $\backslash triangleright\_\{\backslash \{i\backslash \}\}p$ is the prophecy operator defined as $\backslash square\_\{(0,i)\}\backslash neg\; p\backslash land\backslash diamond\_\{(0,i]\}p$ and which states that the first occurrence of $p$ in the future is in $i$ time unit.
• $p\backslash land\backslash square(p\backslash implies\backslash triangleright\_\{\backslash \{1\backslash \}\}p)$ states that $p$ holds exactly at each integral time and not anytime else.

The fragment Safety-MTL_0,v is defined as the subset of MITL_0,∞ containing only formulas in positive normal form where the interval of every until operator has an upper bound. For example, the formula $\backslash Box(a\backslash implies\backslash Diamond\_\{(0,1]\}b)$ which states that each $a$ is followed, less than one time unit later, by a $b$, belongs to this logic.{{cite journal|last1=Bulychev|first1=Peter|last2=David|first2=Alexandre|last3=Larsen|first3=Kim G.|last4=Guangyuan|first4=Li|date=June 2014|title=Efficient controller synthesis for a fragment of MTL_0,∞|journal=Acta Informatica|volume=51|issue=3–4|page=166|doi=10.1007/s00236-013-0189-z|s2cid=253779696 }}

The fragment Open-MTL contains the formula in positive normal form such that:

• for each $\backslash mathcal\; U\_I$, $I$ is open, and
• for each $\backslash mathcal\; R\_I$, $I$ is closed.

The fragment Closed-MITL contains the negation of formulas of Open-MITL.

The fragment Flat-MTL contains the formula in positive normal form such that:

• for each $\backslash phi\_1\backslash mathcal\; U\_I\backslash phi\_2$, if $I$ is unbounded, then $\backslash phi\_1$ is a LTL-formula
• for each $\backslash phi\_1\backslash mathcal\; R\_I\backslash phi\_2$, if $I$ is unbounded, then $\backslash phi\_2$ is a LTL-formula

The fragment Coflat-MITL contains the negation of formulas of Flat-MITL.

Given any fragment L, the fragment L^ns is the restriction of L in which only non strict operators are used.

Given any fragment L, the fragment L_0,∞ is the subset of L where the lower bound of each interval is 0 or the upper bound is infinity. Similarly we denote by L₀ (respectively, L_∞) the subset of L such that the lower bound of each interval is 0 (respectively, the upper bound of each interval is ∞).

Over signals, MITL₀ is as expressive as MITL. This can be proven by applying the following rewriting rules to a MITL formula.{{cite book|last1=Bersani|first1=Marcello|last2=Rossi|first2=Matteo|last3=San Pietro|first3=Pierluigi|title=2013 20th International Symposium on Temporal Representation and Reasoning |chapter=A Tool for Deciding the Satisfiability of Continuous-Time Metric Temporal Logic |date=2013|volume=20|page=202|doi=10.1109/TIME.2013.20|chapter-url=https://re.public.polimi.it/retrieve/handle/11311/964235/49639/BersaniEtAl-CLTLocTool-ActaInf.pdf|hdl=11311/964235|isbn=978-1-4799-2240-6 |hdl-access=free}}

• $\backslash phi\backslash mathcal\; U\_\{(a,b)\}\backslash psi$ is equivalent to $\backslash Box\_\{(0,a]\}\backslash phi\backslash mathcal\; U\backslash psi\backslash land\backslash Diamond\_\{(a,b)\}\backslash psi$ (the construction for half-closed and closed intervals is similar).
• $\backslash Diamond\_\{(a,b)\}\backslash phi$ is equivalent to $\backslash Diamond\_\{(2a-b,a)\}\backslash Box\_\{(0,b-a)\}\backslash Diamond\_\{(0,b-a)\}\backslash phi$ if $2a-b\backslash ge0$.
• $\backslash Diamond\_\{(a,b)\}\backslash phi$ is equivalent to $\backslash Diamond\_\{(a,b-a)\}\backslash Diamond\_\{(0,a)\}\backslash phi$ if
• $\backslash Diamond\_\{(a,+\backslash infty)\}\backslash phi$ is equivalent to $\backslash Box\_\{(0,a)\}\backslash Diamond\backslash phi$.

Applying those rewriting rules exponentially increases the size of the formula. Indeed, the numbers $a$ and $b$ are traditionally written in binary, and those rules should be applied $O\backslash left(\backslash frac\{b\}\{b-a\}\backslash right)$ times.

Contrary to the case of signals, MITL is strictly more expressive than MITL_0,∞. The rewriting rules given above do not apply in the case of timed words because, in order to rewrite $\backslash Diamond\_\{(a,b)\}$ the assumption must be that some event occurs between times 0 and $a$, which is not necessarily the case.

The problem of deciding whether a MITL formula is satisfiable over a signal is EXPSPACE-complete, while satisfiability for MITL_0,∞ is PSPACE-complete.{{cite book|last1=Henzinger|first1=T.A.|last2=Raskin|first2=J.F.|last3=Schobbens|first3=P.-Y.|title=Automata, Languages and Programming |chapter=The regular real-time languages |series=Lecture Notes in Computer Science |date=1998|volume=1443|page=591|doi=10.1007/BFb0055086|isbn=978-3-540-64781-2 }}

R. Alur, T. Feder, and T.A. Henzinger. The Benefits of Relaxing Punctuality. Journal of the ACM, 43(1):116–146, 1996.

R. Alur and T.A. Henzinger. Logics and Models of Real-Time: A Survey. In Proc. REX Workshop, Real-time: Theory in Practice, pages 74–106. LNCS 600, Springer, 1992.

T.A. Henzinger. It's about Time: Real-time Logics Reviewed. In Proc. CONCUR'98, pages 439–454. LNCS 1466, Springer, 1998.

{{Reflist}}

Category:Temporal logic

Category:Model checking