From FSMs to Kripke Structures (exercise sheet 1.b)

Question

b) Construct a propositional logic formula that encodes the set of reachable states 

why (p&!q&!a) is not considered reachable state although it's initial state but (p&a&!q) is considered reachable state?

Answer 1

First, I think the solution should look like this: 

Still, you may have the same question. 

I am afraid that on those exercise sheets the problem was not specified properly. The overall task was there to clean up the Kripke structure, which means to remove all deadend states (recursively) and that would remove that initial state also. In the exam, we will make sure that this is properly stated (and otherwise ask to clarify if you have doubts). 

I would define reachable states as mu y. (Init | <:>y) and the "cleaned up reachable states" as (mu y. (Init | <:>y)) & (nu z.<>z); you may recall that nu z.<>z are the states having an infinite outgoing path. That would give us 

• States(mu y. (Init | <:>y)) = {s0;s1;s4;s5;s6;s7} 
• States(nu z.<>z) = {s1;s3;s5;s7} 
• States((mu y. (Init | <:>y)) & (nu z.<>z)) = {s1;s5;s7}

Answer 2

{p} is a deadend, {p,a} is not a deadend. Hence, {p} is removed from the initial states, while {p,a} is not.

Comments

Still, defining the reachable states as (1) initial states, and (2) existential successor states of reachable states, we should have s0,s1,s4,s5,s6,s7 as reachable states (of the structure you find in my answer).

For reactive systems, we ignore finite paths, and that is a reason to clean up structures in that all finite paths are removed. However, that is another question independent of which states are reachable at first. We should therefore ask rather which states are reachable after removing finite paths.

I would define reachable states as mu y. (Init | <:>y) and the "cleaned up reachable states" as (mu y. (Init | <:>y)) & (nu z.<>z). That would give us

    States(mu y. (Init | <:>y)) = {s0;s1;s4;s5;s6;s7}
    States(nu z.<>z) = {s1;s3;s5;s7}
    States((mu y. (Init | <:>y)) & (nu z.<>z)) = {s1;s5;s7}