Find Universal successor from symbolic representation of Kripke Structure

Question

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

Compute the universal predecessors of p for the corresponding Kripke structure of the FSM.

I am stuck here. Don't know how to proceed. I tried two orders of calculation but ending up with CNF form rather than DNF. How can proceed? Can someone please help?

Answer 1

Well, if you use the teaching tool, it just computes the following:

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

If you want to see the quantification on next(p) in more detail, look at this:

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

Comments

Thank you so much. Now I understood.

Answer 2

The universal predecessors of p is the complement of the existential predecessors of ¬p. In this existential quantification, all cases except for the ones where p' is false, are trivially false. Thus you end up with something like ∃q' false → (…) ∧ a. This is equal to ∃q'  a. As q' doesn't exist here, the quantifier can be ignored. If we now complement this, we get ¬a.

Also look at the handcrafted result in the previous answer.

To get back to your original question: How do you getz from a CNF to a DNF? Simplify, and then multiply out.

Comments

Thank you so much. Now I understood.