LTL about Fp=TUp, is T really necessary in rewriting F?

Question

I just come up with this question. As written in the book of Logic in Computer Science, one of the important equivalence of LTL is this: Fp=TUp. And the T means no constraints.

Yet what if I replace the T with (not p)? Does Fp=(not p)Up hold? Since in this case I actually put some constraints (not p) in the formula, but in the meantime there could be no state can satisfy (not p) and p together. And I tried with different LTL formula as p, and as long as p is satisfiable, then for every path with p, it must satisfy Fp and (not p)Up as well. Does it means that I can rewrite F in this way or there is some counter example?

Answer 1

The short answer:

Yes, both formulas are equivalent and you can rewrite Fp also with (¬p)Up.

and a proof:

We can investigate the problem by looking at the definition of pUq (I think it's defined this way in the book Model Checking by Clarke, Grumberg, Peled).

A path s is a model for the formula (written s ⊨ pUq):

s ⊨ pUq <=>   ∃k: s^k ⊨ q
            ∧ ∀i: 0<=i<k => s^i ⊨ q

(With s^i being the path s with the first i steps removed.)

We have (1):

s ⊨ (¬p)Up <=>   ∃k: s^k ⊨ p
               ∧ ∀i: 0<=i<k => s^i ⊨ ¬p

and (2):

s ⊨ TUp <=>   ∃k: s^k ⊨ p
            ∧ ∀i: 0<=i<k => s^i ⊨ true
        <=>   ∃k: s^k ⊨ p

We want to show (1) <=> (2) (I renamed the ks to k1 and k2 to avoid confusion):

    ∃k1: s^k1 ⊨ p
  ∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p
<=>
    ∃k2: s^k2 ⊨ p

The direction (1) => (2) is trivial.

For (2) => (1) we have to show that from

 ∃k2: s^k2 ⊨ p 

follows

 ∃k1: s^k1 ⊨ p ∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p

We know that there exists a value for k1 (namely k2) such that s^k1 ⊨ p holds. But what about the second part? We can now just use for k1 the smallest value such that s^i ⊨ p holds. Then the second part is true, because if there would be an i such that s^i ⊨ not p does not hold, we know that s^i |= p holds. But in that case we would have choosen i for k1 because i is strictly smaller then k1.

So both formulas (1) and (2) are equivalent.