# Temporal Logic

Are these two examples correct? Only one of the two formulas should be satisfied. I got different answer. Just for my confidence I would like to ask if my answer is also correct? Because I am mostly getting different answers for these types of questions. Thanks a lot in advance.

Question 8 (a), (b). +1 vote

(G a)⊕(F !a) holds on the structure, and ((X G a)⊕(G !a)) does not hold on the structure, so yes, the first example is an example structure that distinguishes between the two formulas.

In the second example, I am not sure what formulas you exactly mean, but despite of that, you are also right, since our teaching tool tells us the following:

• (G b) -> F[a WU b] is valid
• (G b) -> [(F a) WU b] is valid
• (G b) -> ![(G b) SU a] is not valid
• (G b) -> !G[b SU a] is not valid
by (142k points)
ok. Thank you so much.
Can you please tell me how can I generate such answers in the online tool?
You can use the LTL theorem prover (https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html) for this. You can state that two formulas are equivalent and will obtain a counterexample if they are not.
Ok. Thank you :) It would be really helpful.