Exercise Sheet 5 - Question 1.b

Question

Compute the Kripke structure K={I′,S′,R′,L′}K={I′,S′,R′,L′}of 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=!p&!q,
R=R=a&p&next(p)&next(q)|a&q&!p&!next(p)&!next(q)|a&!p&!q&!next(q)&next(p),
and the following Kripke Structure and state transition diagram.

    

b) Construct a propositional logic formula that encodes the set of reachable states S'_{reach of} Kripke Structure.

my answer - (a&!p&!q)|(p&!q&!a)|(p&a&!q)

It says wrong in the tool. Could any one help me on this, where I did the mistake.?

Answer 1

Your kripke structure is correct but the set of reachable states is incomplete. You are missing two more states. the states {p,q} and {p,q,a} are also reachable states since they are the successors of a reachable state {p,a}.

Comments

Thank You! I was having the idea that the states will be considered as reachable states only if its direct successors of initial state.

Answer 2

Your reachable states differ from the Kripke structure you drew. From state {a, p}, you can reach {p,q} and {p,q,a}.

See also: https://q2a.cs.uni-kl.de/887/exercise-sheet-5-question-1

Comments

Got it, Thank You!