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

529 users

0 votes

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 ?

in * TF "Emb. Sys. and Rob." by (790 points)
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

1 Answer

+1 vote
 
Best answer

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.

by (166k points)
selected by
!(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.

Related questions

Imprint | Privacy Policy
...