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

972 questions

1.1k answers


469 users

0 votes
February 16, 2022, 7e

In my eyes, S2 is satisfied in the path s0->s1 where there exists a path where finally (!a & EGa ) holds. Please help me understand how S1 distinguishes S2.
in # Study-Organisation (Master) by (850 points)

1 Answer

0 votes
The formula !a&EGa cannot hold in any state since it is a contradiction. You can see that by unrolling EGa into a & EX EG a which then contradicts directly !a. Hence, S2 is simply false and cannot hold in any state.

EGa holds in state s0, but not in state s1. Consider now E(F!a & Era) which is equivalent to (EF!a)&(EGa). This holds in state s0 since the path s0->s1^omega satisfies F!a and the path s0^omega satisfies EGa. Hence, s0 satisfies (EF!a)&(EGa), but s1 does not. Finally, abbreviate this formula by a new variable b which is therefore a label of s0, but not of s1, and consider the formula EGb. It clearly holds in s0, but not in s1, and therefore S1 holds in s0.
by (147k points)

Related questions

Imprint | Privacy Policy