Of course, there are algorithms for deciding the equivalence of CTL*, LTL and CTL formulas. In essence, these algorithms work as follows: They are all based on the recursive laws of the operators, i.e.,
- [a SU b] = b | a & X[a SU b]
- [a WU b] = b | a & X[a SU b]
- G a = a & X(G a)
- F b = b | X(F b)
After this, you may check with satisfiabiliy of propositional logic whether that makes a difference for the present point of time, and if so, the formulas are not equivalent. Otherwise, you continue with the formulas behind the X-operator to check the equivalence for the future points in time.
After finitely many steps, a situation already seen must occur again, and here we can close a loop. Then, we need to check for the strong operators SU and F whether their even b becomes true on that infinite path or not. This is the analogon to checking least and greatest fixpoints in local model checking.
Sometimes that procedure may also make sense for these exam problems, but usually that is too much work. It is better to carefully read the formula, then to single out things that don't matter and abstracting the rest.
For instance, consider the two formulas
- XX(G(a⨁b)⨁F(a<->b))
- XX(G(a⨁b)|G(a<->b))
The first thing you may recognize is that both formulas start with XX, so we may just look into what comes later, so that we consider now
- G(a⨁b) ⨁ F(a<->b)
- G(a⨁b) | G(a<->b)
Next, both formulas have an occurence of G(a⨁b), but the first one has then F(a<->b) while the other one has G(a<->b). Note that ¬(a<->b) = (a⨁b) and ¬(a⨁b) = (a<->b) holds, thus we can replace (a<->b) by (a<->b) = ¬¬(a<->b) = ¬(a⨁b), so we get next
- G(a⨁b) ⨁ F¬(a⨁b)
- G(a⨁b) | G¬(a⨁b)
At that point, it makes sense to abstract away from (a⨁b), e.g., let's call it p, i.e., p := (a⨁b), so that we now consider
Finally, note that ¬G p = F¬p and ¬F p = G¬p holds, hence, we get
Now, what do these formulas say? The first one is simple true, since for any q, we have q⨁¬q. So, when is the second formula not true? The second formula states that p always holds or ¬p always holds, ie. where p is constantly true or false.
So, to make it false, choose any path where p changes its value at least once, and working backwards that gives you a desired counterexample for the original formula.
These kinds of exam problems simply require some logic reasoning and thinking about the formulas. That usually allows one to simplify matters, and then it is not that difficult to get a counterexample. How to proceed in particular, depends on the given example, and that requires then some experience.
