Greatest simulation relation [closed]

Question

In Problem 3.c of Aug 2018 paper, we have been asked to find greatest simulation between K1<=K2.

From SIM1 -

s0q0, s0q3, s0q1, s1q0, s1q1, s1q3, s2q2, s3q0, s3q1, s3q3, s4q0, s4q1, s4q3 and s5q5

From SIM2 -

Step 1- s0q0, s0q1, s0q3 should be removed because s0 - {} (no successors). But the solution is contradicting to my understanding.

The solution has s0q0/q1/q3. Is the solution incorrect?

Answer 1

You mean s5q2 in SIM1, I guess.

No, the solution is correct as far as I can say. For checking whether K1<=K2 holds, you have to check the following diagrams:

    S0 --> {}
    |     
    Q0 --> {Q1;Q3}


    S0 --> {}
    |     
    Q1 --> {Q0;Q2}


    S0 --> {}
    |     
    Q3 --> {Q1}


    S1 --> {S0;S2}
    |     
    Q0 --> {Q1;Q3}


    S1 --> {S0;S2}
    |     
    Q1 --> {Q0;Q2}


    S1 --> {S0;S2}
    |     
    Q3 --> {Q1}


    S2 --> {S0;S3}
    |     
    Q2 --> {Q0}


    S3 --> {S0;S4}
    |     
    Q0 --> {Q1;Q3}


    S3 --> {S0;S4}
    |     
    Q1 --> {Q0;Q2}


    S3 --> {S0;S4}
    |     
    Q3 --> {Q1}


    S4 --> {S0;S5}
    |     
    Q0 --> {Q1;Q3}


    S4 --> {S0;S5}
    |     
    Q1 --> {Q0;Q2}


    S4 --> {S0;S5}
    |     
    Q3 --> {Q1}


    S5 --> {S0}
    |     
    Q2 --> {Q0}

Checking a diagram means to check whether for every state s1' in the upper right corner, you find a state s2' in the lower right corner such that (s1',s2') are in the current relation. So, if the set in the upper right corner is empty, you don't have to check anything, and things are fine.

Comments

Thanks a ton!!