I have some doubts regarding the SIM2 property of Greatest Simulation and Greatest Bisimulation.

As per the definition, SIM2 must hold if:

for s1,s1' ∈ S1,s2 ∈ S2 with (s1,s2) ∈ σ and (s1,s1') ∈ R1

there must be s2' ∈ S2 with (s1 ,s2') ∈ σ and (s2,s2') ∈ R2

1. What has to be done if s1 does not have any successors [if s1 is dead state] and s2 is having successors? [Can we retain this pair?]

s1--------{}

s2--------{p1}

2. What has to be done if s2 does not have any successors [if s2 is dead state] and s1 is having successors? [Can we retain this pair?]

s1--------{p1}

s2--------{}

3. Both s1 and s2 are dead states? [Can we retain this pair?]

s1--------{}

s2--------{}