# Kripke Structures: one of the node in pairs of SIM1 has no successor

+1 vote
I would like to clarify on elimination of pairs if one of the node has no successor.

Scenario 1. Simulation

example pair (s1,q1) . S1 has no successors but q1 has some successor. In this case there is no need to delete pair right?

Scenario 2: Simulation

example pair (s1,q1). S1 has successors but q1 has no successors.In this case, the pair has to be deleted since q1 cannot simulate s1 isnt it?

Scenario 3: Bisimulation

example:

example pair (s1,q1) . S1 has no successors but q1 has some successor. pair is to be deleted right?

Scenario 4: Bisimulation

example pair (s1,q1). S1 has successors but q1 has no successors. In this case also, pair is to be deleted right?

Scenario 5: Bisimulation or Simulation

when both the nodes of pair has no successors. Then the pair always survives right?

If a state S1 has no successors, then all of its successors satisfy any criteria – including the criterion that each of them are in relation with a successor of Q1.

If a state S1 has no successors, then it can not provide any successors that could be in relation with a successors of Q1.

If both of them have no successors, then there is no successor left to complain about not having a successor to be in relation with.
by (25.6k points)

Scenario 1. Simulation
example pair (s1,q1) . S1 has no successors but q1 has some successor. In this case there is no need to delete pair right?

Correct. We just have to check that every transition s1 can do can also be simulated by q1. Since s1 has no transitions, q1 has nothing to care about.

Scenario 2: Simulation
example pair (s1,q1). S1 has successors but q1 has no successors.In this case, the pair has to be deleted since q1 cannot simulate s1 isnt it?

Correct. In that case the transitions s1 can do must also be simulated by q1, but since q1 has no successors, it cannot simulate any transition s1 has. Thus, the pair will be eliminated next.

Scenario 3: Bisimulation
example pair (s1,q1) . S1 has no successors but q1 has some successor. pair is to be deleted right?

Correct. In that case the transitions q1 can do must also be simulated by s1, but since s1 has no successors, it cannot simulate any transition q1 has. Thus, the pair will be eliminated next.

Scenario 4: Bisimulation
example pair (s1,q1). S1 has successors but q1 has no successors. In this case also, pair is to be deleted right?

Correct. In that case the transitions s1 can do must also be simulated by q1, but since q1 has no successors, it cannot simulate any transition s1 has. Thus, the pair will be eliminated next.

Scenario 5: Bisimulation or Simulation
when both the nodes of pair has no successors. Then the pair always survives right?
Right.
by (166k points)