Exercise Sheet 5 - Question 1.b

0 votes

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.?

2 Answers

0 votes
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}.
by (1k points)
Thank You! I was having the idea that the states will be considered as reachable states only if its direct successors of initial state.
0 votes
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
by (25.6k points)
Got it, Thank You!

0 votes
2 answers
0 votes
1 answer
0 votes
1 answer
0 votes
2 answers
0 votes
2 answers