TPTL is More Expressive than MTL

Abstract: TPTL and MTL are two extensions of the linear-time temporal logic LTL geared towards the expression of quantitative properties. In TPTL, timing constraints are expressed using freeze-quantifiers, while in MTL, they are attached to the "Until" modality. In [BCM05], we prove that TPTL is strictly more expressive than MTL, as conjectured by Alur and Henzinger in [AH92] and [AH93].

Timed linear-time temporal logics.

Linear-time temporal logic is a formalism for expressing qualitative properties about the executions of a system. A formula in that logic is built from atomic propositions, standard boolean operators, and modalities. The main modality is called Until, denoted by U, with the following semantics: an execution satisfies "φUψ" if, along the execution, there exists a point where ψ holds, and such that all intermediate positions satisfy φ.

In the late 80's, this logic has been extended to reason about quantitative properties of these executions. We focus here on the following two:

  • modalities decorated with quantitative constraints: In that logic, we write "φU[a,b]ψ" for expressing that φ holds until ψ holds, with the extra condition that the witnessing ψ must occur between a and b time units after the current position. In the sequel, we use obvious abbreviations, such as "φU≥2ψ" instead of "φU[2,∞)ψ".

    The resulting logic is called MTL [Koy90].

  • freeze-quantification: In that logic, we use extra clocks (named formula clocks) for specifying temporal constraints. The syntax is as follows:

    φ ::= p | x ∈ [a,b] | ¬ φ | φ ∨ φ | φ U φ | x. φ

    where [a,b] is an interval with rational bounds.

    The resulting logic is named TPTL [AH89].

There are several different semantics for timed logics. In our case, we assume that the underlying time domain is the set of nonnegative reals, and consider two different semantics:

  • point-based semantics: In that framework, formulas are evaluated along timed words, i.e. sequences of pairs (p,t) where p is a set of atomic propositions and t is the (rational) date of occurence of event p. The formal semantics is defined as follows (boolean operators are omitted):
    MTL      (pi,ti), j |= p     iff     p ∈ pj
    (pi,ti), j |= φ U[a,b] ψ     iff     ∃k>0.   ∑j+1..k ti ∈ [a,b]   and
    (pi,ti), j+k |= ψ   and
    ∀0<m<k.   (pi,ti), j+m |= φ
    TPTL      (pi,ti), j, α |= p     iff     p ∈ pj
    (pi,ti), j, α |= x ∈ [a,b]     iff     α(x) ∈ [a,b]
    (pi,ti), j, α |= x. φ     iff     (pi,ti), j, α[x←0] |= φ
    (pi,ti), j, α |= φ U ψ     iff     ∃k>0.   (pi,ti), k, α+∑0..k tj+1+i |= ψ   and
    ∀0<m<k.   (pi,ti), m, α+∑0..m tj+1+i |= φ
    where α is a valuation of formula clocks, &alpha[x←0] is the valuation α where clock x has been reset, and &alpha+t is the valuation β : x → α(x)+t.

    A formula φ ∈ MTL holds along a path (pi,ti) whenever (pi,ti), 0 |= φ.
    A formula φ ∈ TPTL holds along a path (pi,ti) whenever (pi,ti), 0, &alpha0 |= φ, where α0 : x &rarr 0.

  • interval-based semantics: The interval-based semantics is a really continuous semantics, where formulas are evaluated along timed state sequences, i.e. sequences of pairs (pi, Li) where Li are contiguous, non-overlapping intervals with rational bounds, forming a partition of the set of nonnegative reals. A timed state sequence naturally defines a function π from the nonnegative reals to the subsets of atomic propositions, defined with π(t) = pj where j is the unique integer s.t. t ∈ Lj. Now, the interval-based semantics is defined as follows:
    MTL      π, t |= p     iff     p ∈ π(t)
    π, t |= φ U[a,b] ψ     iff     ∃t'∈[a,b].   π, t+t' |= ψ   and
    ∀0<u<t'.   π, t+u |= φ
    TPTL      π, t, α |= p     iff     p ∈ π(t)
    π, t, α |= x ∈ [a,b]     iff     α(x) ∈ [a,b]
    π, t, α |= x. φ     iff     π, t, α[x←0] |= φ
    π, t, α |= φ U ψ     iff     ∃t'>0.   π, t+t', α+t' |= ψ   and
    ∀0<u<t'.   π, t+u, α+u |= φ

    A formula φ ∈ MTL holds along a path (pi,Li) whenever π, 0 |= φ.
    A formula φ ∈ TPTL holds along a path (pi,Li) whenever π, 0, &alpha0 |= φ.

The conjecture.

Clearly enough, any formula expressed in MTL can be translated into an equivalent TPTL formula: formula "φ U[a,b] ψ" is equivalent to "x. φ U (ψ ∧ x∈[a,b])". The converse inclusion has been conjectured, but had never been proved:

Conjecture:  [AH92,AH93]
  • TPTL is strictly more expressive than MTL;
  • The following TPTL formula cannot be expressed in MTL:

    G( a → x. F ( b ∧ F( c ∧ x≤2 ) ) )

A surprising formula.

It turns out that the second point of the conjecture is wrong, at least when considering the interval-based semantics: Indeed, it is equivalent to the following MTL formula:

  /    F≤1b ∧ F=1 F≤1 c
 | ∨
G    a →  |     F≤1(b ∧ F≤1 c)
 | ∨
  \    F≤1(F≤1 b ∧ F=1 c)

This formula is obtained by distinguishing between three cases:

  • First, the case where b occurs before 1 t.u. and c occurs after 1 t.u. from a.
  • Second, the case where both b and c occur before 1 t.u. In that case, in particular, c occurs at most 1 t.u. after b. This is precisely what the second line expresses.
  • Last, the case where both b and c occur between 1 and 2 t.u. In that case, precisely 1 t.u. before c, we know that at most 1 t.u. elapsed, and that a b must occur within 1 t.u.

So, is TPTL really more expressive than MTL?

Theorem:  [BCM05]
  • TPTL is strictly more expressive than MTL;
  • The following TPTL formula cannot be expressed in MTL:

    x. F( (a ∧ x≤1) ∧ G( x≤1 → ¬b ) )

This TPTL formula means that the last atomic proposition before time point 1 is an a. This can be reformulated in MTL+Past as follows:

F=1( ¬b S a )
Even if it is not strictly equivalent, this formula distinguishes between the models we use in the proof. This immediately gives the following corollary:

Corollary: MTL+Past is strictly more expressive than MTL.

The proof.

We prove the result for the interval-based semantics.

We will use the following standard technique: build two families of timed state sequences that are distinguished by our TPTL formula (i.e. it will hold on all the items of one family and fail to hold on the other one), and prove that no MTL can distinguish between them (i.e. that any MTL formula has the same value on both paths). In fact, we have to restrict the MTL formulas we consider: Indeed, if two paths differ at time point t, it is easy to write an MTL formula that distinguishes them, by using modality F=t.

We will use the following two paths, with two parameters p and n that will be defined later (we simply require that p=1/m for some positive integer m, and n is a positive integer):

Two families of timed state sequences

Red lines indicate positions where a holds (for both sequences, at time points (1+2k)p/(4n) for any nonnegative integer k), while green lines indicate positions where b holds ((k+1)p/2-7p/12n for the first path (which will be denoted by Ap,n in the sequel) and (k+1)p/2-p/12n for the second one (which will be denoted by Bp,n in the sequel), k being any nonnegative integer. Note that our TPTL formula does hold along Ap,n and fails to hold along Bp,n, whatever the values of p and n.

Let φ be an MTL formula. We define the following two values:

  • p is the granularity of the formula, defined formally as follows:
    p = ∏ 1 
    q/r ∈ φr
  • n is the temporal height of the formula, i.e. the maximal number of nested Until modalities.

We claim the following lemma:

Lemma: Any MTL formula with granularity p and temporal height n cannot distinguish between Ap,n+3 and Bp,n+3.

The proof of that lemma is by induction on the structure of the MTL formula. In order to simplify the proof, we may assume that p and 0 are the only constants that appears in the formula. The technical details can be found in [BCM05].

Now, assume that our initial TPTL formula has an equivalent MTL formula. If p is the granularity of that formula and n is its temporal height, then that formula cannot distinguish between the two corresponding sequences, which is contradictory with the fact that it is equivalent to the original TPTL formula.

Now, if we assume the point-based semantics, we keep the same trajectories (seeing them as timed words). A similar proof shows that the same lemma holds, hence the result.

Additional comments.

  • The result is robust w.r.t. strictness of Until.
  • The result still holds for TPTL(F,G) vs. MTL.
  • The original formula proposed by Alur and Henzinger can be proved to be inexpressible in MTL when assuming the point-based semantics.
  • The result extends to TCTL with clocks vs. TCTL with subscripts.

 

References

[AH89]       R. Alur and T. A. Henzinger. A Really Temporal Logic. In Proceedings of the 30th Annual Symposium on Foundations of Computer Science (FOCS'89), pages 164-169. IEEE Computer Society Press, 1989.
[AH92]       R. Alur and T. A. Henzinger. Logics and Models of Real-Time: A Survey. In Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74-106. Springer-Verlag, 1992.
[AH93]       R. Alur and T. A. Henzinger. Real-Time Logics: Complexity and Expressiveness. Information and Computation 104(1), pages 35-77. Elsevier, 1993.
[BCM05]       P. Bouyer, F. Chevalier and N. Markey. On the Expressiveness of TPTL and MTL. Research report LSV-2005-05. Lab. Spécification et Vérification, May 2005.
[Koy90]       R. Koymans. Specifying Real-Time Properties with Metric Temporal Logic Real-Time Systems 2(4), pages 255-299. Kluwer, 1990.

About LSV