CODEWITHSUNDEEP
logicverificationprooftemporalmodel-checking
Becky L
Becky L

Reputation: 31

Linear Temporal Logic (LTL) questions

[] = always

O = next

! = negation

<> = eventually

Wondering is it []<> is that equivalent to just []?

Also having a hard time understanding how to distribute temporal logic.

  1. [][] (a OR !b)

  2. !<>(!a AND b)

  3. []([] a ==> <> b)

Upvotes: 1

Views: 802

Answers (2)

nondeterministic
nondeterministic

Reputation: 521

G p indicates that at all times p holds. GF p indidcates that at all times, eventually p will hold. So while the infinite trace pppppp... satisfies both of the specifications, an infinite trace of the form p(!p)(!p!)p(!p)p... satisfies only GF p but not G p.

To be clear, both these example traces need to contain infinitely many locations, where p holds. But in the case of GF p, and only in this case, it is acceptable that there be locations in between, where p does not hold.

So the short answer to the above question by counterexample is: no, those two specifications aren't the same.

Upvotes: 0

Bromind
Bromind

Reputation: 1128

I'll use the following notations:

F = eventually
G = always
X = next
U = until

In my model-checking course, we defined LTL the following way:

LTL: p | φ ∩ ψ | ¬φ | Xφ | φ U ψ

With F being a syntactic sugar for :

F (future)
Fφ = True U φ

and G:

G (global)
Gφ = ¬F¬φ

With that, your question is :

Is it true that : Gφ ?= GFφ

GFφ <=> G (True U φ)

Knowing that :

P ⊧ φ U ψ <=> exists i >= 0: P_(>= i) ⊧ ψ AND forall 0 <= j < i : P_(<= j) ⊧ φ

From that, we can clearly see that GFφ indicates that it must always be true that φ will be always be verified after some time i, and before that (j before i) True must be verified (trivial).
But Gφ indicates that φ must always be true, "from now to forever" and not "from i to forever".

Upvotes: 2

Related Questions