!!Compute the deadends

Question

What does it mean when it says Compute the deadends?

deadends are states how they should get computed?

Answer 1

Deadend states are states without outgoing transitions. If you have symbolic transition relation R(x,x'), then the set of deadend states can be computed as ¬∃x'.R(x,x'), i.e., 

∃next(a).∃next(o).∃next(p).∃next(q).(q|(a->next(p)))&!(next(q)->o|p)&true
  = ∃next(o).∃next(p).∃next(q).!(next(q)->o|p)&(q|(a->next(p)))
  = ∃next(p).∃next(q).!(next(q)->o|p)&(q|(a->next(p)))
  = ∃next(q).!(next(q)->o|p)|!(next(q)->o|p)&(q|!a)
  = !(o|p)|!(o|p)&(q|!a)

Comments

Because next(a) and next(o) is not included in symbolic formular, they can be excluded. For exist next(q) and exist next(p), how can you transform? Also, could you give me the reason why you add &true to the end of the formular?