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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes


According to the explanation given for EG!a above, I did not understand why is there a need for s0->s1? Doesn't the path s0->s2 satisfies EG!a as well? Can someone explain this? 

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

1 Answer

0 votes
If you will drop the transition s0->s1, then there is no longer a path starting in s0 that would satisfy G!a, so that EG!a is then no longer true in s0. To satisfy property S1, we need both the paths s0->s1^omega as well as s0->s2^omega. For the outermost E of E(Fb & EG!a), we use the path s0->s2^omega which satisfies Fb & EG!a since b is reached on s2, and in state s0, we also have EG!a (because the other path is there).

So, property S1 holds in s0, but property S2 does not.
by (170k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...