sheet 5 Question 5

Question

The question is- for the following Kripke structure, Minimize K by the quotient construction.

Submit the solution in the following form:

vars a,b,c,d;

init 0;

labels 0:a; 1:a,b; 2:a,b; 3:c; 4:c; 5:d;
transitions 0->1; 0->2; 1->3; 2->4; 2->5; 3->3; 4->4; 5->5;

My answer: the minimized structure is - 

 =>    

The minimized diagram is -  

 

Final submitted answer : vars c,d;

init 1,2;

labels 1:; 2:c,d; 3:;

transitions 1->1; 1->3; 3->1; 3->2; 2->1; 

It is showing the wrong format error while submitting it on the portal. Please help me where am I wrong?

Answer 1

As far as I can see, your solution is almost correct. First of all, you just have listed a wrong set of variables (it should be a,c,d instead of c,d). If no state has label a, it means that a is false in all of these states, it does not mean that a does not exist!

Finally, we have

    {(S0,S0);(S1,S1);(S2,S2);(S3,S3);(S4,S4);(S5,S5)} 
    ∪ {(S0,S3);(S1,S4);(S2,S5)}
    ∪ {(S3,S0);(S4,S1);(S5,S2)}

so that we can merge states {(S0,S3);(S1,S4);(S2,S5)}

As we have three states, we call them 0,1,2 and have then the following structure that we obtain by renaming 3 by 0, 4 by 1 and 5 by 2:

vars a,c,d;
init 0,2;
labels 0:; 1:; 2:c,d;
transitions 
    0->0; 0->1;
    1->0; 1->2;
    2->0; 

So, it seems that your second problem was that you named states 1,2,3 instead of 0,1,2. Am I right?

Comments

Yes, you were right. I named the states wrong (1,2,3) instead of (0,1,2). It worked! thanks.