What are steps to compute the universal and existential successor of the following FSM symbolically?

Question

A=(2Vin,2Vout,φI,2Vstate,φR) where Vin={a}Vout={o}Vstate={p,q}φI=p∨q
φR= next(p)<->!(next(q)->(o|q->(a<->p))).Existential successors of !(a&p) for the corresponding Kripke structure of the FSM.

Answer 1

In general, the existential successors of a state set φQ under a transition relation φR are computed as new2old(∃x1....∃xn.(φR∧φQ) where the function new2old replaces all variables x' to encode the target states by their corresponding variable x used to encode the current state.

To compute the set of states, the quantifiers in the above formula have to be eliminated which is done by their definition, i.e., ∃x.φ is replaced with φ[x<-0] ∨ φ[x<-1] (which is the disjunction of the cofactors by x). It is recommended to plan the right variable ordering in which the quantifiers are eliminated: While the result will be the same, the work may significantly differ. Moreover, the following rules are often useful and applied below without mentioning:

• x∧φ = x∧φ[x<-1]
• ¬x∧φ = ¬x∧φ[x<-0]
• x∨φ = x∨φ[x<-0]
• ¬x∨φ = ¬x∨φ[x<-1].

In the particular example, we have the following:

new2old(∃p.∃q.∃a.∃o.(next(p)<->¬(next(q)->(o ∨ q->(a<->p))))∧¬(a∧p))
  = new2old(∃p.∃q.∃o.
        (next(p)<->¬(next(q)->(o ∨ q->(0<->p))))∧¬(0∧p)  ∨ 
        (next(p)<->¬(next(q)->(o ∨ q->(1<->p))))∧¬(1∧p)
    )
  = new2old(∃p.∃q.∃o.
        (next(p)<->¬(next(q)->(o ∨ q->¬p)))  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))∧¬p
    )
  = new2old(∃q.∃o.
        (next(p)<->¬(next(q)->(o ∨ q->¬0)))  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))∧¬0  ∨ 
        (next(p)<->¬(next(q)->(o ∨ q->¬1)))  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))∧¬1
    )
  = new2old(∃q.∃o.
        (next(p)<->¬(next(q)->1))  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))
    )
  = new2old(∃q.∃o.
        (next(p)<->0)  ∨ 
        (next(p)<->¬(next(q)->¬(o ∨ q)))
    )
  = new2old(∃q.∃o.
        ¬next(p)  ∨ 
        (¬(next(q)->¬o∧¬q))
    )
  = new2old(∃q.
        ¬next(p)  ∨ 
        (¬(next(q)->¬0∧¬q))  ∨ 
        (¬(next(q)->¬1∧¬q))
    )
  = new2old(∃q.
        ¬next(p)  ∨ 
        (¬(next(q)->¬q))  ∨ 
        next(q)
    )
  = new2old(∃q.
        ¬next(p)  ∨ 
        (¬(0->¬q))  ∨ 
        next(q)
    )
  = new2old(∃q. ¬next(p)  ∨  next(q) )
  = new2old( ¬next(p)  ∨  next(q) )
  = ¬p  ∨  q

Apart from this, one may of course also use the BDD algorithms for quantifier elimination. In the above example, we obtain the following BDD for the conjunction of the transition relation and the state set (where next(p) and next(q) are written as p1 and q1, respectively):

While it is a lot of work to construct this BDD, it is maybe interesting to point out that we don't need to have it in full detail, and therefore it would be enough to make a Shannon decomposition by q1 and p1. Since all variables are quantified out except for q1 and p1, all paths leaving nodes labeled with p1 lead to the 1-leaf. This will eliminate the leftmost node of p1 and will then give us the final result: 

However, the use of BDD algorithms is not recommended for manual computations, in the computer, it would however usually be the most efficient way to solve the problem. 

Comments

(next(p)<->¬(next(q)->(o ∨ q->(1<->p))))∧¬(1∧p) = (next(p)<->¬(next(q)->¬(o ∨ q)))∧¬p

as we know that 1<->p=p, then how the outcome of (o ∨ q->(1<->p)) is equal ¬(o ∨ q) ?

---

Okay, let's do that in more detail:

      (next(p)<->¬(next(q)->(o ∨ q->(1<->p))))∧¬(1∧p)
    = (next(p)<->¬(next(q)->(o ∨ q->(1<->p))))∧¬p
    
Now, we can use ¬p∧φ = ¬p∧φ[p<-0]

    = (next(p)<->¬(next(q)->(o ∨ q->(1<->0))))∧¬p
    = (next(p)<->¬(next(q)->(o ∨ q->0)))∧¬p

and φ->0 is equivalent to ¬φ∨0, i.e., ¬φ, we have

    = (next(p)<->¬(next(q)->¬(o∨q)))∧¬p

---

Thanks a lot Sir

Answer 2

It should be noted that there are exercise sessions where these questions are answered in great detail. If you still have questions in or after the exercise session you are always welcome to ask your question and may some of your peers will also benefit from that.
If you in general are looking for a solution for your special task to verify your answer, it is recommended to use the provided training tools. Please make sure to use them only for validation purposes and not as a substition for doing the exercises "by hand".

Best regards