You are given two formulas S1 and S2, in your case, these are the formulas [b WU [a WU c]] and [b WU [a SU c]], respectively. You should understand the difference of the given formulas in that you should be able to say when one holds but the other does not hold.
To this end, you must first decide whether you want to show that we have S1&!S2 or !S1&S2. If S1&!S2 should hold, you should find two formulas phi1 and phi2, such that
- phi1 is not equivalent to phi2, i.e., phi1<->phi2 is not valid; this makes sure that you really have found two formulas and that one is just a minor syntactic change of the other one like phi1 & true
- phi1 and phi2 are both satisfiable, i.e., neither !phi1 nor !phi2 are valid; this avoids that you could simply use false as one of the formulas (which could otherwise always be used)
- neither phi1 nor phi2 is equivalent to S1&!S2; this avoids that you use simply S1&!S2 as one of the formulas (which could otherwise always be used)
- finally, phi1->S1&!S2 and also phi2->S1&!S2 is valid; this shows that S1 holds under the conditions described by phi1 and phi2, while S2 does not hold (hence, phi1 and ph2 point out two nontrivial conditions to show the difference of the two formulas)
How to find such formulas? Best would be to carefully read and understand them, and the to figure out two conditions ph1 and phi2 as described above.
An automated way without much creativity would work as follows: If we would try to prove S1->S2 and this would not be true, then a proof tool will give you a counterexample which is a path that must satisfy S1&!S2. Using teaching tools, you can find such a counterexample.
Then, you need to express the path, i.e., the counterexample, as an LTL formula phi1.
After this, you need to find a second formula. Again that should be a counterexample to the validity of S1->S2, but trying that again with the same tool will give you the same answer as before. Thus, you need to tell the tool to produce another counterexample which can be done by proving !phi1 & S1 -> S2, since the tool will then produce a counterexample that will satisfy !phi1 & S1 & !S2. Again, it remains to specify that counterexample as an LTL formula.
That is it. You just have to make sure that your formulas at the end meet the above requirements, and therefore, before submitting them, you should double-check whether the requirements hold.
