2021.02.17.vrs.solutions.pdf: Problem2 (a)Simulation and Bisimulation - Miniminzation

Question

Hello Professor,

Two Doubts:
1. Since S2 has no outgoing edges, in step 1 all the states like example: S0,S1 gets removed. Is this right?

2. In step 3, (which is not shown in the solution) , S3, S4 is included because (s0,s4) and the reverse transition (s4,s0) are both included in step 2 to satisfy bisimulation. (s0,s1) does not hold in step2. But that is ok as one of the pairs should satisfy and also the reverse should satisfy for that pair. Is my understanding right?

Best Regards,

Answer 1

We get the following diagrams for this example:

    S0 --> {S1;S3}
    |   
    S1 --> {S2}

    S0 --> {S1;S3}
    |    
    S2 --> {}

    S0 --> {S1;S3}
    |    
    S3 --> {S0;S1}

    S0 --> {S1;S3}
    |    
    S4 --> {S1;S4}

    S1 --> {S2}
    |    
    S2 --> {}

    S1 --> {S2}
    |    
    S3 --> {S0;S1}

    S1 --> {S2}
    |    
    S4 --> {S1;S4}

    S2 --> {}
    |    
    S3 --> {S0;S1}

    S2 --> {}
    |    
    S4 --> {S1;S4}

    S3 --> {S0;S1}
    |    
    S4 --> {S1;S4}

We remove (S0,S2) since we would have to find for one of S1 or S3 a related successor state of S2. As this does not exist, we remove (S0,S2). Also, we remove (S1,S2) since S1 has the successor S2 but we find no related successor for S2. Since we compute a bisimulation, we have to find for each one of the successor states in the lower right set a related state in the upper right set. For this reason, we remove For removing (S2,S3) and (S2,S4) and so on.

(S3,S4) remains in the relation since we have (S0,S4) and (S1,S1) in the relation when checking that for any state of the upper set there is one in the lower set, and for checking that for any state of the lower set there is one in the upper set, we find (S1,S1) and (S4,S0).