LTL equivalence

Question

Hello,

I have some trouble solving the LTL equivalence exercise. There are given the two formulas:

S1=[[a WU b] WU c] and
 

S2=[[a WU b] SU c]

I tried the answer: "1 ; G a; G (a & b)" which i verified with the online training tool. But the online exercise system told me that both formulas are not correct. Are there some mistakes regarding the syntax or did I miss something else?

Thanks for your help

Comments

I think the problem is how you believe to have verified your answer with the online tool.

Both of your answers do allow c in the first step which satisfied both S1 and S2.

Answer 1

Consider the given formulas S1 = [[a WU b] WU c] and S2 = [[a WU b] SU c]. First note that S2 implies S1, i.e., [[a WU b] SU c] -> [[a WU b] WU c] since the strong until implies the weak until. However, the converse implication, i.e., [[a WU b] WU c] -> [[a WU b] SU c] is not valid: As a counterexample, consider a path where we have G(a&!b&!c) such that [a WU b] and therefore also [[a WU b] WU c] hold from the initial point of time on. Since c never holds, [[a WU b] SU c] is however false which is the difference between weak and strong until.

The exercise wants you to determine two formulas (different to false) that show the difference between the two formulas, i.e., that imply S1&!S2. Your answer was "1 ; G a; G (a & b)" which means that you claim that the following should hold:

1. (G a) -> [[a WU b] WU c] & ![[a WU b] SU c] 
2. (G(a&b)) -> [[a WU b] WU c] & ![[a WU b] SU c] 

However, both implications are not valid: A counterexample for the first one is G(a&!b&c) since then (G a), [a WU b], [[a WU b] WU c], and [[a WU b] SU c] are all true from the beginning. A counterexample for the second implication is G(a&b&c) so that (G(a&b)), [a WU b], [[a WU b] WU c], and [[a WU b] SU c] are again all true from the beginning. Hence, both implications are false. 

I guess that you have verified something else with the tool. What you need are two formulas that imply [[a WU b] WU c] & ![[a WU b] SU c], i.e., that satisfy [[a WU b] WU c], but not [[a WU b] SU c]. One of the two should be clear from what is written above. However, I should not give the complete solution to the exercise here, and leave the rest up to you. 

Answer 2

As already mentioned, there is most likely a flaw in your verification. What is important to note is that by a LTL formula we describe a set of paths. Therefor G a restricts the set of all paths S over the given set of variables to the set S \ F !a, so all the paths where for each timestep a holds (while everything else is unrestricted).
By this follows that some of your paths in the set [G a] satisfy both formulas, like for example G (a&b&c), while some paths only satisfy S1 e.g. G (a&b&!c). Note that G (a&b&c) → G a and is therefore a subset of paths.

A way to reason about this, is that by not restricting certain variables x you allow all possible combinations of them and to make sure that this does not conflict with your goal of finding a set of paths where ALL of these paths satisfy a certain property (which is in this specific case that all paths should satisfy S1 but not S2).