simulation of products kripke - problem 2.b August 2021 exam

Question

In the answers sheet, in the second step why are we not removing any of the tuples?
Should we consider both of the K1 and K2 in the predecessor checking procedure?
Would you please briefly explain the solution?

Answer 1

For the given structures, we have to consider the following diagrams in that we have to check in case the states on the left column are in the relation that for each one of the transitions in the upper line, there is a corresponding one in the lower line where "corresponding" means that the states we consider in the second column are in the relation.

Note the diagrams list all successors of the states in the rows, and the left column lists pairs of states that have the same labels, i.e., are initially in the relation we consider. 

    P0Q0 --> {P0Q0;P1Q1;P2Q2}
    |    
    Q0 --> {Q0;Q1;Q3}

(P0Q0,Q0) is in the relation of step 1, so we have to check whether for each state {P0Q0;P1Q1;P2Q2}, there is a corresponding one in {Q0;Q1;Q3} which is the case: (P0Q0,Q0),(P1Q1,Q1),(P2Q2,Q2). Hence, (P0Q0,Q0) remains in the relation.

    P1Q1 --> {P2Q2}
    |    
    Q1 --> {Q2}

(P1Q1,Q1) is in the relation of step 1, so we have to check whether for each state {P2Q2}, there is a corresponding one in {Q2} which is the case: (P2Q2,Q2). Hence, (P1Q1,Q1) remains in the relation.

    P1Q1 --> {P2Q2}
    |    
    Q4 --> {Q0;Q4;Q5}

(P1Q1,Q4) was already removed, so we don't have to consider that one again.

    P2Q2 --> {P1Q1}
    |    
    Q2 --> {Q1;Q2}

(P2Q2,Q2) is in the relation of step 1, so we have to check whether for each state {P1Q1}, there is a corresponding one in {Q1;Q2} which is the case: (P1Q1,Q1). Hence, (P2Q2,Q2) remains in the relation.

    P2Q2 --> {}
    |    
    Q3 --> {Q3}

(P2Q2,Q3) is in the relation of step 1, so we have to check whether for each state {}, there is a corresponding one in {Q3} which is trivially the case. Hence, (P2Q2,Q3) remains in the relation.

    P1Q4 --> {}
    |    
    Q1 --> {Q2}

(P1Q4,Q1) is in the relation of step 1, so we have to check whether for each state {}, there is a corresponding one in {Q1} which is trivially the case. Hence, (P1Q4,Q1) remains in the relation.

    P1Q4 --> {}
    |    
    Q4 --> {Q0;Q4;Q5}

(P1Q4,Q4) is in the relation of step 1, so we have to check whether for each state {}, there is a corresponding one in {Q4} which is trivially the case. Hence, (P1Q4,Q4) remains in the relation.

    P1Q5 --> {P2Q2}
    |    
    Q5 --> {Q2}

(P1Q5,Q5) is in the relation of step 1, so we have to check whether for each state {P2Q2}, there is a corresponding one in {Q2} which is the case:(P2Q2,Q2). Hence, (P1Q5,Q5) remains in the relation.