Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

543 users

0 votes


φ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?

in * TF "Vis. and Sci. Comp." by (870 points)
edited by

1 Answer

+1 vote

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).

by (166k points)
Thank you so much. I was replacing new2old first and then doing existential quantification. I understood now.
Imprint | Privacy Policy
...