Computing deadends from kripke strucrue

Question

I am trying to compute the deadends and reachable states from the following kripke structure and i get the following:

deadends: !p&!q&!a | !p&!q&a | !p&q&!a | !p&q&a | p&q&!a | p&q&a

reachable states: p&!q&a | p&!q&!a | p&q&!a | p&q&a

But the tool rejects it as being incorrect, am i missing something ?

Comments

How did you create that Kripke structure? Maybe your answer can be found on https://q2a.cs.uni-kl.de/802/converting-given-automaton-to-kripke-structure?show=817#a817 already?

---

I used the tool https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html to convert the given fsm transition relation to a kripke structure. These were the parameters i used:
state variables: p;q;a;o
input variables :
initial states: !(p->q)
transition relation: (o|a->!(p->q))&next(q)&next(p)
state set: false
This generates the diagram above and i computed the deadends and reachable states as shown in the question.

In the answer posted here: https://q2a.cs.uni-kl.de/802/converting-given-automaton-to-kripke-structure , the fsm is right but the kripke structure doesn't correspond to what i generated from the tool

Answer 1

The deadend states are those where pre∀(false) holds, so I can let the same tool compute them. If I do so, I get 

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

which is equivalent to

• q&a|q&o|!p&a|!p&o

and that is not equivalent to your result. Please check.

Comments

!(a|o->!(p->q)) is equivalent to !p&!q&!a&o|p&q&a&o|p&q&a&!o|p&q&!a&o|!p&q&a&o|!p&q&a&!o|!p&q&!a&o|!p&!q&a&o|!p&!q&a&!o.

why did we ignore the rest and only pick q&a|q&o|!p&a|!p&o.

All of them correspond to deadends

---

We don't ignore them and pick some. The two formulas are equivalent to each other. Both are DNFs but DNFs are not canonical. To get the represented states of a formula, you have to consider its satisfying assignments, and those correspond to the midterms of a full DNF. Otherwise you have don't cares that you have to expand. For instance, q&a is not one state but four since q&a is equivalent to q&a&!p&!o | q&a&!p&o | q&a&p&!o |q&a&p&o.