# [Temporal Logics] LTL Equivalence (exercise sheet 8 question 1)

I have watched the videos and also read the questions that other students asked. But I'm totally clueless and have no idea what this assignment wants and what I should do!!! Could you please help me and explain it in an easy beginner way?

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

1. 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
2. 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)
3. 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)
4. 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.

by (170k points)
selected by
So as far as I understood, in my case phi1 could be: G(a&!b&!c)
and for phi2, I gave !(G(a&!b&!c)) & [b WU [a WU c]] -> [b WU [a SU c]] to the tool and received:
__q2,__q1,a
__q2,__q1,b,a
So how exactly should I write it as phi2?
I wrote the final solution this way and it wan't correct!
1; G(a&!b&!c); (a&b&!c)|(a&!b&!c)
Using case 1 is right, and the first formula, i.e., G(a&!b&!c) is also fine. The second formula does not describe the counterexample you have seen. That one is an infinite path that alternates between two states (a&!b&!c) and (a&b&!c). You just allow that the initial state is either  (a&!b&!c) or (a&b&!c), and all other states on the path are arbitrary. That is not the counterexample. Think twice, and (before submitting try the teaching tool to verify your answer).
A little hint is maybe okay: Why not writing phi2 as follows: (a&!b&!c) & X(a&b&!c) & G(...)? Then the first state and the second state are as they should be. Inside the missing part of the Always-formula you have to make sure that this continues.