Simulation of two kripke structures

Question

When finding successor of pairs in any of steps we have three different scenarios

1. S1 -> {s2} P1 -> {}

2. S2 -> {} P2 -> {P1}

3. S2 -> {} P2 -> {}

Is there any rule to automatically exclude or include these pairs into steps to find the fix points.

Answer 1

Your question is how the general rule specializes to the cases where sets of states are empty. To this end, recall that a universal quantification over an empty set is trivially true, while an existential quantification over an empty set is trivially false. 

The condition that retains a pair of states (s1,s2)∈Hi in the relation Hi during the fixpoint computation of the greatest simulation relation is 

    ∀s1′∈S1. ∃s2′∈S2. (s1,s1′)∈R1 → (s2,s2′)∈R2 ∧ (s1′,s2′)∈Hi

which can also be written equivalently as follows:

    ∀s1′∈S1. (s1,s1′)∈R1 → ∃s2′∈S2. (s2,s2′)∈R2 ∧ (s1′,s2′)∈Hi

or even simpler as

    ∀s1′∈succ(s1). ∃s2′∈succ(s2). (s1′,s2′)∈Hi

The above condition simplifies for empty successor sets as follows:

1. If succ(s1)={}, the above condition simplifies to true, so all pairs (s1,s2) where succ(s1)={} holds is retained in the relation.
2. If succ(s1)!={} and succ(s2)={}, the above condition simplifies to false, so all pairs (s1,s2) where succ(s2)={} holds is removed from the relation.