Simulation and Bisimulation

Question

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--------{}

Answer 1

This question has already been answered before: https://q2a.cs.uni-kl.de/2787/query-regarding-simulation-and-bisimulation

If s1 does not have successors, nothing has to be checked, and SIM2 holds. If s1 does have successors, but s2 does not have successors, SIM2 does obviously not hold.

Comments

Thanks, I understood the point.