# Exercise sheet 5 Problem 1C 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.

related to an answer for: exercise sheet 5 question 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)

by (138k points)
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!

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.

by (160 points)
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.