LTL to LTL

Question

August 2021 - 8a - A small clarification

[a U GF(b)]

= (a SU b) V Gb

= (a SU b) V (true SU a)

I tried to write this as solution. Is it also valid solution?If not please explain.

From lecture i understand LTL has  only pure path formulas state formulas:  P ::= VΣ  I was trying to satisfy.

Answer 1

Your solution is not correct. You are right that LTL formulas must not have path quantifiers, so your formulas are LTL formulas. However, the formulas are not equivalent to each other:

Just consider a transition system with a single state with a self-loop where a holds but where b is false. Then, [a WU G F b] holds on the single path of that structure while both [a SU b] and G b are false.

Also for the second equivalence, [true SU a] is equivalent to F a, but not to G b. You can check the equivalence of LTL formulas with https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html