Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


538 users

0 votes

In this translation, how is one X removed?

I have done this:

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


in * TF "Emb. Sys. and Rob." by (370 points)


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

Doubt in translating to CTL - [CS@TUK] Questions and Answers (

1 Answer

+1 vote

[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)

by (166k points)
Thank you. It's clear now

Related questions

0 votes
2 answers
asked Jan 15, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy