# Correct Counterexamples for formula

Hey there,

Like in Problem 7 of the last exam (2.2017) I can follow the given solution, but I am not sure if mine is also correct. Can someone just check them and give maybe short comments? Would the explanation below be sufficient to get the points in the exam?

**a)**

s1 is satisfied, because on all paths Ga or F!a holds

s2 is not satisfied, because the path 0(2)^w does not hold, since Ga is false and !a is also false in the initial state.

**b)**

[$\phi$ SU $\psi$] is only true, if we have $\phi$*$\psi$, which means, that somewhere $\psi$ must hold.

[$\phi$ WU $\psi$] on the other side is also true, if we have only $\phi$.

Therefore s1 is not satisfied, because b never holds.The same is true for s2 except we have GFa here and in state 1 a holds indeed infinity often. So s2 is satisfied

**c)**

S1 is satisfied, because IF at some time t a holds, in t+1 b must hold.

S2 is not satisfied, because in the next Step (which is one after the initial state) a has to hold if and only if b holds finally. But we are in an endless loop of b, so a cannot hold. The right example doesn't show this, since in the next step a holds and then we reach the b-loop.

**d)**

S2 is satisfied, because on all paths (we obviously have only one path) infinity often !b holds.

S1 is not satisfied, because there is no path, where after one step and some time finally !b holds always.

**e)**

b never holds, so according to my understanding above [c SU b] never becomes true. This leads to A[ false SU a] which should be false as well. Therefore S2 is not satisfied. (Would it be satisfied, if the initial state is empty, which means false? Then [false SU c] would hold).

S1 is satisfied, because we have a sub-path (initial state) with only one c, which satisfies [c WU b] and then reach a.

In e) I am not 100% sure.. Thanks in advance for help.