Computing set of states that satisfy a formula

Question

1) Compute the set of states that satisfy AG(EXb ∨ E [c SB c])

2) Compute the set of states that satisfy EX(E [b SU a] ∨ A [c U c])

In question 1, the solution says the formula [c SB c] is false, because c before c is an invalid condition. Hence we ignore it.

In question 2, the solution says A [c U c] is just A(c).

I was confused why this holds because c weak until c seems false but i think it is true because in a U b, Ga satisfies it

Answer 1

• [ c WU c ] is the same as c. So is [ c SU c] the same as c. The reason is that the right hand subformula of [ c SU c ] is satisfied at the moment the left hand one is satisfied. If you don't have c in the first step, then the left side is not satisfied (which is has to as long as the right hand side isn't satisfied). So the formula is not valid but satisfiable.
• [ c SB c ] has no satisfying path. Since it is a strong before, the left side needs to be satisfied. But that would already satisfy the right hand side, which may only happen after the left hand side has been satisfied. Thus, the formula is not satisfiable (and thus definitely not valid)
• [ c WB c ] has satisfying paths. Namely those paths that never satisfy c. Since the right hand condition is never satisfied, the Before is not violated. As it is a weak before, the left hand side doesn't need to be satisfied. Thus, it is non valid but yet satisfiable.