Exam 14-02-2018, Question 9a

Question

In this translation, how is one X removed?

I have done this:

Where did I go wrong? In the sample solution the G(a ⊕b) is neglected. why so?

 

Comments

Hi,

Please take a look, for the first part, below explanation might help.

Doubt in translating to CTL - [CS@TUK] Questions and Answers (uni-kl.de)

Answer 1

[true SU a] is not equivalent to (F a) | (G a), instead it is equivalent to F a only, and therefore no G(a⊕b) is generated at all. The solution could also be as follows:

        ¬E(X X X G F G F ¬([true SU (a ⊕ b)])) 

    <-> ¬E(X X X G F G F ¬F (a ⊕ b)) 

    <-> ¬E(X X X G F G F G ¬(a ⊕ b)) 

    <-> ¬E(X X X F G ¬(a ⊕ b)) 

    <-> ¬E(F G ¬(a ⊕ b)) 

    <-> A G F (a ⊕ b)

    <-> A G A F (a ⊕ b)

Comments

Thank you. It's clear now