You derive the symbolic description of the automaton by determining any propositional logic formula for its transition relation, i.e., any propositional logic formula whose satisfying assignments are the transitions of the automaton. The simplest formula you may derive is a DNF of the transitions. In the above case, that means
!p&!next(p) | p&!a&next(p) | p&a&!next(p)
Note that this formula is equivalent to next(p) <-> p&!a (as listed in the above figure).
