# Simulation and Bisimulation

In a Kripke structure K1 , if we have state s0 with {a} and a state s1 with {d} and in Kripke structure K2, if we have state q0 with {a,b,d} and another state {a,d}, in step so, do we take pairs of all these states like :

step0; {s0, q0}, {s0,q1} , {s1, q0 ), (s1,q1)

Or do we take state pairs with exactly the same value ?

Hey,

As can be seen in chapter 4 (Transition Systems) on page 17, the following pairs of states are checked:  (s1 , s2 ) ∈ σ implies L1 (s1 ) ∩ V2 = L2 (s2 ) ∩ V1

For your example you have to check which set of variables is given for the Kripke structures.

Assume you have the variable set {a,d} given for K1 and {a,b.d} given for K2, this would mean that there is no state pair matching this property.
by (440 points)

We take pairs of states with exactly the same observable label. Observable means that you  first have to remove all variables of a structure that are not know by the other structure and vice versa. After that the labels must be exactly the same for generating the pairs of step 0.

by (166k points)