Product of Two Kripke Structures - Exercise 4 - Q 4

Question

Hello

I am trying to find the product of two Kripke structures using the Tool

vars b,c,d;

init 0;

labels 0:; 1:d;

transitions 0->0; 0->1; 1->0

vars b,c,d;

init 0;

labels 0:b,c; 1:b,c,d; 2:b,c,d;

transitions 0->1; 0->0; 1->0; 1->2; 2->0

But I am not getting any response, I am getting no answer using the tool https://es.cs.uni-kl.de/tools/teaching/BisimulationQuotients.html, only a blank space.

Could anyone please help.

Thanks

Answer 1

Well, that is so, since the product structure of the structures you have given to the tool does not have any state. Note that none of the pairs of states has a consistent labels.

Looking at your exercise, I see, however, that the first structure is actually only defined on variable d and not on b,c,d as the second structure. If you change that, the tool will give probably what you expect.

Comments

Thanks a Lot. Now I am getting the answer in the tool.