FSMs to Kripke Structures Q3 [closed]

Consider the FSM: A={2Vin,2Vout,I,2Vstate,R}A={2Vin,2Vout,I,2Vstate,R}
where Vin={a}Vin={a}Vout={}Vout={}Vstate={p,q}Vstate={p,q}φI=φI=q,
φR=φR=a&p&!q&!next(p)&next(q)|p&q&next(p)&next(q)|p&!a&!q&next(p)&next(q),
and the following state transition diagram:
s0: {}s1: {p}s2: {q}{a}/{}s3: {p,q}{}/{}{}/{}{a}/{}

construct the state transition diagram for the corresponding Kripke structure of the given FSM, and solve the following tasks.

Above is the question that I have got.

After solving the above problem;

I get below Kripke structure after removing deadends and unreachable states -

vars a,p,q;

init 0,1;

lablels 0:p,q; 1:p,q,a;

transitions 0->0; 0->1; 1->0; 1->1;

And I get deadend as - {}, {q}, {a}, {q,a}

What's wrong in it?

closed with the note: Answer solved

closed

With your remark I see the problem and edited this answer. Let's have a look at the following FSM where the reachable states are given in green color:

We construct the following Kripke structure for this FSM:

Now, you can clearly see that:

• deadend states are s0,s1,s4,s5
• states with only finite outgoing paths are s0,s1,s4,s5,s6
• initial states are s1,s3,s5,s7
• initial states with at least one outgoing infinite path are s3,s7
• reachable states are s1,s3,s5,s7
• reachable states with at least one outgoing infinite path are s3,s7

There is a trouble with this kind of exercise that I try to clarify for years. Some exercises use "deadend state" as "state with only finite outgoing paths", so try that as an alternative solution. I guess that is your trouble here, and I would rather agree with your solution.

by (147k points)
edited by
Thanks, but thats not how I'm asked to submit answer. I have to construct a Kripke structure out of the corresponding state diagram. My Kripke structure has 8 states - {}, {a}, {p}, {q}, {pq}, {pa}, {qa}, {pqa},

After solving this, I got

intial states = {pq}, {pqa}
deadends as {}, {a}, {q}, {qa}.

But I'm getting the answer for deadends incorrect.
Brill, this works! Thank you! But do we also have to memorize these for exams?
In the exams, we will make sure that we are precisely using the definitions!
Can I ask how? I have same problem and it is still checked as wrong :(
I checked your submission and you entered something like s0 ∨ s1∨ ... . However, you have to submit a formula using the variables of the Kripke structure, i.e., a,p,q.