Simulation or Bi Simulation Related Query

Question

This is regarding Kripke Structures Simulation, Bi-simulation, etc.

​

In exam, we are asked to find if the simulation or Bi-simulation holds or not.

​

Suppose, during solving, in intermediate steps, I find that the initial set state pair is no more a part of state pairs, then I can stop further finding the fixpoint and it can be concluded that it will not hold even if the fixpoint is reached as initial state set pair was removed in intermediate steps. Can we do it this way to save time in the exam?

Below is the example, After step 2, (P2,Q2) & (P4,Q2) are removed which are initial states pair.

We could have stopped and concluded that it won't hold without looking for fixpoint.​

Answer 1

Of course you can do that! And the same idea also applies to model-checking, i.e., if a least fixpoint is computed and all initial states are already included, you may stop since you already have the answer.