2023.02.15.vrs.solutions.pdf: Product Structures, Simulation and Bisimulation

Question

Protokol: 2023.02.15.vrs.solutions.pdf

For the fix point to be reached step1 should be same as step0. Here in the Problem 2(a) part, I cannot get (S2,Q1) into step1 while solving it by myself.

Could you explain why should we include  (S2,Q1) in the step1?

Best Regards,

Answer 1

After setting up the initial relation, we have to repeatedly check the simulation diagrams which look as follows:

    s --> {s1;...,sM}
    | 
    q --> {q1;...,qN}

We need to check whether for every state s1;...,sM is in relation to one of the states q1;...;qN. In case of the particular example, there are the following diagrams to check:

    S0 --> {S2}
    |     
    Q0 --> {Q1}


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


    S2 --> {}
    |     
    Q1 --> {Q3}


    S3 --> {S2}
    |     
    Q0 --> {Q1}


    S4 --> {S2;S3;S5}
    |     
    Q2 --> {Q0;Q1;Q3}


    S5 --> {S0;S3}
    |     
    Q3 --> {Q0}

For the pair (S2,Q1) there is no state in the upper right corner, so that there is nothing to check. Such pairs of states will always remain in the relation.