Hi,

Given a Kripke structure K={V,φI,φR}K={V,φI,φR}

where V={a,b,c}V={a,b,c}, φI=φI=!(b<->a), φR=φR=next(a)&a&(b|b<->next(c)).

the task is: "Compute the set of states from which the states satisfy **!b** can be reached symbolically, and submit the solution in **disjunctive normal form**."

As I understand the question, the task is to compute the existential predecessors of **!b**, which would result in the following:

∃next(a).∃next(b).∃next(c).next(a)&a&(b|b<->next(c))&!next(b)
= ∃next(b).∃next(c).!next(b)&a&(b<->next(c))
= ∃next(c).a&(b<->next(c))
= a&b|a&!b

However, neither **a&b&c|a&b&!c|a&!b&c|a&!b&!c ** nor **a **is accepted as a solution.

Do I understand something about the question wrong?