Kripke structure 3

Question

why are the reachable states q | !p & !q which are supposed to be the successor of the reachable states S3?

Answer 1

I understood the solution but still dont get why we cant answer with the kripke state like this: a | (p & q & a) | (q & a)

Comments

Well, the two formulas are simply not equivalent to each other. Your formula a | (p & q & a) | (q & a) is equivalent to "a", so that it holds in the four states labeled with "a". However, state s4 is not reachable, but is labeled with "a", and s1 is reachable, but not labeled with "a".

Answer 2

The Kripke structure of the FSM is the following one:

The classification of the states is as follows:

• initial states: {s2,s3,s6,s7}

• reachable states: {s0,s1,s2,s3,s6,s7}

• dead(end) states: {s1,s3,s5,s7}

• finally dead(end) states: {s1,s3,s5,s7}

Hence, the reachable states are all except for {s4,s5} so that the reachable states can be encoded as !(a&p&!q | !a&p&!q) which is equivalent to !(p&!q). The latter is equivalent to !p|q and also equivalent to q|!p&!q.

Comments

thank you so much for your detailed answer. Could you please explain the occurrence of node s1 in the chart above?I thought that the value of a must be always true to satisfy the transition condition R.

---

That is not a contradiction: The transition relation a&next(p)&next(q) states that from all states where a holds, there is a transition to the state where p&q holds. Since the next value of "a" is not relevant, each state where "a" holds has a transition to state !a&p&q and another one to state a&p&q. These are all transitions encoded by the transition relation.