Symbolic computation of predecessor and successor

Question

We have a FSM: =(2Vin,2Vout,φ,2Vstate,φ)A=(2Vin,2Vout,φI,2Vstate,φR), where Vin={a}Vin={a}, Vout={o}Vout={o}, Vstate={p,q}Vstate={p,q}, φ=p∨qφI=p∨q, φ=φR=((a->next(p)&(q|p))<->next(q))&o

How to compute the existential predecessors of !(q->a) step by step?

Answer 1

Using https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html, you will get the following:

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

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

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

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

  = o&!a|o&(a->p|q)

Remember the definition of the boolean quantification, and in many cases, one of the cofactor becomes trivial.