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?
