Simulation and Bisimulation

Question

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 ?

Answer 1

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.

Answer 2

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.