Temporal Logic

Question

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.

Exam paper: https://es.cs.uni-kl.de/teaching/vrs/exams/2018.02.14.vrs/2018.02.14.vrs.solutions.pdf

Question 8 (a), (b).

Answer 1

(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

Comments

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.