Doubt regarding Kripke

Question

Here we need to do bisim with respect to K0 itself.

I got the states, like that, but in the diagram I'm bit confused. 

Here from s5 I can go to only s1. But when we combined the states s0 and s1, can s5 go to the combined state? Since it can't go to s0. Could please help on this?

Answer 1

Since s0 and s1 turn out to be bisimilar, we cannot distinguish these states by any mu-calculus formula without past modalities <:> and [:]. That means whether s5 makes a transition to s1 or to s0 does not matter, since from there, we can do the same things.

If we would allow past modalities (as in the full mu-calculus), your concern must be considered, which is why we then have to consider a stronger kind of bisimulation (see lecture notes).

Comments

So,
Question 1)
if we have only one state in the quotient state, and if it satisfy any of the combination states of others , which mean {(s2,s3) , (s0,s1)} has predecessor s5 or in other words s5 can go to either s2 or s3 in (s2,s3) or s0 or s1 in (s0,s1) then I can draw the the transition from s5 to those combined states, is the right?

Question 2)
 if i have combined state like (s0,s1) and (s2,s3) then, if i want to draw a transition from (s0,s1) to (s2,s3) , then s0 should go to s2 or s3 , similarly s1 also go to s2 or s3. if one of them is missing then , i can't draw the transition. is that right?

Question 3) If from (s0,s1) , only s0 if going to s5 and s1 is not going to s5 , can i draw the transition?

Question 4) (s0,s1) and (s2,s3) , if s0 is going to both s2 and s3 , but s1 is dead end. Can i draw the transition.?

Question 4) (s0,s1) and (s2,s3) , if s0 and s1 are  going to s2 . But not to s3(s3 does not have any predecessor). Can i draw the transition.?

---

Question 1): Yes, if states s[i] and s[j] are bisimilar, we do not distinguish them anymore. You can create a new name S[i,j] and use that new state instead of the previous ones. That means the new state inherits all transitions of the states it contains.

Question 2): For the transitions of the quotient structure, have a look at the definition of the quotient structure on page 45 of VRS-04-TransitionSystems: There is a transition between quotient states S1 and S2, if these sets of states contain states s1 and s2 which are connected by a transition. It does not matter if other states in S1 have a transition to s2, it is enough if there are two such states s1 and s2 in S1 and S2, respectively.

Question 3): As explained in the answer of Question 2: (S1,S2)∈Rq :⇔ ∃s1∈S1.∃s2∈S2.(s1,s2)∈R

Maybe consider the structure from this description:

    s0->s1; s0->s2;
    s1->s0; s1->s3;
    s2->s4;
    s3->s4;
    s4->s5;
    s5->s1;

We now merge s1:=s0 and s3:=s2 in that I rename these accordingly:

    s0->s0; s0->s2;
    s0->s0; s0->s2;
    s2->s4;
    s2->s4;
    s4->s5;
    s5->s0;

---

Yeah. I understood, since it's a bisimulation we can simulate one using others. Thanks for the clarification