Kripke Structure Reachable States [closed]

Question

I am trying to define the reacheble states for the following graph:

In my FSM, the initial state had to satisfy p.

According to the exercise session presentation for exercise 4, page 4, we need to remove deadends from the set of initial states (even though this doesn't really make sense according to the definition in the lecture VRS04-p8). Therefore, p&!q&a&0 would not be an initial state, even though it satisfies p (the condition described by the FSM). Therefore, my initial states have to satisfy p&!a. The student portal accepts this as a correct answer.

I'm now trying to find all reachable states. According to this comment, reachable are those states that lie on an infinite path from an initial state. Therefore, the reachable states in my example should be p&!a, since they lie on an infinite path starting from themselfes with "p,q" However, this does not get accepted as a correct solution. Why?

Edit: Here is my FSM whose transitions got accepted by the student portal:

Edit 2: I found my mistake. I drew the wrong Kripke graph. This is the right one:

Answer 1

A definition that I found for unreachable states is that unreachable states are states that are not reachable from an initial state. That means a state should be reachable from an initial state and that explains why state "q" is accepted. I can't give you a complete answer about the other states that got accepted since I don't have the other information about the FSM. Even in the exercise slide, one state that was a deadend is added in the reachable states.

Comments

Sadly, p&!a | !p&q&!a&!o (with the last one being the formula for "q") doesn't work.
I edited my question to include the FSM.

---

!p&q&!a&!o is not the same formula as q. q seen as a formula describes all states in which q is true, so half the states of the Kripke structure. All the other variables are don't care because they don't occur in it, i.e. {p,q,a} would also be a state represented by the formula q, but not included in your diagram.

---

@choehne in fact !p&q&!a&!o is the formula where q is true and the other variables are false. If sschwarz had written only q than this will include even the other variables that we don't care, representing other states that have q true but not given in the Kripke structure. This brings me to the point that you can try to write the formula by giving all the variables and not just writing p&!a because this will include even other states that are not reachable.

Answer 2

When I did the exercise, the exercise system did accept my solution for the reachable states only when I also included those states that are lying on finite paths, e.g. deadend states. So in your case, the correct solution should be p&!a | !p&q&!a&!o , i.e. all states that you drew.

Comments

I tried p&!a | !p&q&!a&!o, but that didn't work :/