Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

0 votes
I am trying to compute the product of two Kripke structures of the following form:

K1: vars a,c,d;

init 0,1;

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

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


K2: vars b,c,d;

init 2;

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

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

i tried with both hand and tool to solve the product and this is the resultant Kripse Structure I get (after eliminating the unreachable state and its edges):

K1*K2= vars a,c,d;

init 0;

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

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

But the Solution is not getting accepted by the exercise automated checker. Am i doing something wrong here?

Please help!
in * TF "Emb. Sys. and Rob." by (150 points)

1 Answer

0 votes
Best answer
If K1 is defined on variables a,c,d and K2 is defined on variables b,c,d, then their product is defined on variables a,b,c,d .
by (166k points)
selected by
Thank you KS. adding b to the list of variables worked.
I had removed the variable "b" as it was belonging to the unreachable state SQ2.
Yes, I have seen what you thought. But even though there is no state left which carries variable b, it is still known by the product and the states of the product state that b is false there. Not mentioned means false and not that it does not exist. It's a common mistake, I know.

Related questions

0 votes
1 answer
asked Aug 15, 2020 in * TF "Emb. Sys. and Rob." by SKH (350 points)
+1 vote
1 answer
0 votes
1 answer
asked May 23, 2023 in * TF "Emb. Sys. and Rob." by farwinr (380 points)
Imprint | Privacy Policy