Of course, this is possible!
However, there is no general recipe (except for converting the formulas to automata and checking their equivalence, which is what the teaching tool does).
In most cases, we can do this with less effort. For example, consider the following two formulas:
- S1 = [[c WU b] WU a]
- S2 = [[c SU b] SU a]
Obviously, we are being asked for the difference between WU and SU, and we can find this out by substituting one for the other to see the difference. Remember from the lecture that, in general, we have
- [x WU y] = [x SU y] | G x
- [x SU y] = [x WU y] & F y
So S2 will be false if we always have "!a", while S1 is equivalent to G[c WU b]. So we have to satisfy the latter, which is easily done by G b.
So, a formula that implies S1&!S2 is G(!a&b).
If you really don't see how to start, you may try the recursion laws of one of the temporal operators, to see what must hold now and next. That often reveals different requirements of the two given formulas that tell you how two distinguish between the two.
