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 ?