Thanks.Yes I had done wrong labelling. Could you please check the Kripke structure and the states?

Question

Comments

Actually I found the right answer(variable O is not needed). my deadends are  {},{q} but the system says its wrong. and reachable states are {p},{p,a},{p,q},{p,q,a} and {q}. This also wrong. could you please check it?

---

Drawing the Kripke structure is not recommended here since it has already quite some states. You can answer the questions also directly with the FSM. However, there are more deadends than {},{q}. The FSM has these deadend states, but the Kripke structure has more deadend states like also {a},{a,o},{p,o},{p,a,o},{p,q,o},{p,q,a,o}. Also, there are more reachable states. You suggest p&!q&a|p&!q&!a|p&q&!a|p&q&a|!p&q&!a which is equivalent to q&!a|p, but there are also the reachable states !p&q&a.

---

But the question says (Compute the deadends for the corresponding Kripke structure of the FSM ) thats the reason why I went for a kripke structure. but the complete Kripke structure is too big if I am to construct it from my R equation and all the variables. this is the clean format resulted from the FSM and the variables that are only true in the transitions. Can I use the big Kripke structure to answer the question then? I saw a post already where you are creating the complete kripke and the clean one. I will try anyway.

---

Clearly, you can compute the Kripke structure to answer the questions, but that is more work than needed. Just consider slide 11 of chapter 4, where you can find the following dead(s ) :⇔ ¬∃s′ ∈ SKripke. (s, s′) ∈ RKripke ⇔ ¬∃s′ ∈ SKripke. (state(s), input(s), output(s), state(s′)) ∈ RFSM. Hence, you need to check in the FSM whether there is a state s, with an input and an output which does not have a successor state. That is all what you need; just list them all and write the result in form of a DNF.

---

Thank you, I will check it.

Answer 1

Well, that makes sense to me, but why do you not just submit the solution and let the system check whether you are right, instead of me? I think your solution is fine, be brave and submit it.

Comments

I did and it says wrong. I don't understand where am I going wrong.