Exercise sheet 5 Problem 1C

Question

Above is my kripke structure from the FSM. I am stuck in problem number 1c. So far according to my understanding following is my result. But, somehow this is wrong. 

( p&!q&!a&!next(p)&next(q) | p&q&!a&!next(p)&next(q) ) & !next(a)

May be I am getting wrong at the last part of the answer. I tried this many times, but can not find any solution. So, far my understanding is I am excluding all the deadends. But, why still this is wrong. Help please.

Answer 1

Since you have only listed the transition relation, I have to guess the initial states of your exercise. Looking at your solution, it seems that the initial states are described by the formula q. 

If I am right with this assumption, you have to consider the following state transition system:

That is indeed easy to see if you multiply out the formula of the transition relation: Then you get exactly the two transitions that you can see in the diagram above also:

• p&!q&!a&!next(p)&next(q)& !next(a)
• p&q&!a&!next(p)&next(q)& !next(a)

Comments

But still I stuck. I used
p&!q&!a&!next(p)&next(q)& !next(a) | p&q&!a&!next(p)&next(q)& !next(a)
for the answer 1.c but this is also wrong. I understand this. But, what the mistake here? For more clarification I am giving the details below:

Compute the Kripke structure K={I′,S′,R′,L′}of the FSM: A={2Vin,2Vout,I,2Vstate,R}
where Vin={a}, Vout={}, Vstate={p,q}, I=q,
R=p&!a&!next(p)&next(q)|!a&!p&!next(p)&!next(q),

1.a) p&q&!a | !p&q&!a
1.b) p&q&!a | !p&q&!a | !p&!q&!a | !p&q&a | !p&!q&a

a and b answers are correct. But, still can't find the mistake for C and D.

Update:
I have found my mistake. And shared as a different post here!

Answer 2

At last I have got my solution. I did one mistake while I derived the kripke structure. I have missed one edge which will be from empty state to a state. After doing this, I have got my solution. 

Whenever I asked question I did not share the question, that was my another mistake. Sorry about this. By the way, thank you for your clarification.  

Comments

Can you explain how does it make a difference?

---

In empty state for the self loop my input and output was {}/{} in the trasition diagram. That is why for kripke I had to draw two transitions: one will be the self loop and another will go to the state a.The reason was I have to go where p and q both would be false. I drawn the self loop but other transition was missing towards the state a.