Question

What if we were checking  the reverse K2<= k1?

Would that also be the same? we still consider the deadend states?

Best Regards,

Answer 1

For the reverse, we consider again the diagrams, but have to find for each state in the lower successor set a related one in the upper successor set. Now consider the following diagram:

    S2 --> {}
    |     
    Q1 --> {Q3}

We therefore have to find for Q3 are related state in {} which obviously does not exist. So, we would remove the pair (S2,Q1) if we would check for bisimulation or the reverse simulation.