Find existential successor from Symbolic representation of FSM

Question

φR= !(((a->o)->p|q)<->next(q))&next(p)

Compute the existential successors of true&!p = !p  for the corresponding Kripke structure of the FSM.

If we use the definition of existential successor then the last element in transition relation &next(p) and Q relation !p will form &p&!p which will make existential successor always false. How can we calculate in such cases? Also I am facing the same situation for univesal successor calculation.

Can someone please help?

Answer 1

Well, false is also a result and means that there are no such states. In the above example, you get empty sets of states for the predecessors, however, instead of the successors as you said. When I am using the teaching tool, I can quickly calculate all successor and predecessor states as follows:

EXISTENTIAL PREDECESSORS (PRE∃)

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

Note that false is equivalent to false (hence no states).

UNIVERSAL PREDECESSORS (PRE∀)

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

Note that false is equivalent to false (hence no states).

EXISTENTIAL SUCCESSORS (SUC∃)

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

Note that !(!(a->o)<->q)&p|!q&p is equivalent to p&!q&!o&!a | p&!q&o&!a | p&!q&!o&a | p&q&o&a | p&q&o&!a | p&q&!o&!a | p&!q&o&a (seven states).

UNIVERSAL SUCCESSORS (SUC∀)

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

Note that !(!q&p) is equivalent to !p&!q&o&a | !p&!q&o&!a | !p&!q&!o&a | !p&!q&!o&!a | p&q&o&a | p&q&o&!a | p&q&!o&a | p&q&!o&!a | !p&q&o&a | !p&q&o&!a | !p&q&!o&a | !p&q&!o&!a (12 states).

Comments

Thank you so much. I was replacing new2old first and then doing existential quantification. I understood now.