Product of Kripke Structures 14th Feb 2018 Paper

Question

In the below, why is state b is not taken in the final structure.

As per Professor's explanation in the video(Product Structures), we are checking for variable b to be true and multiplying with the states where b is true as well, so should ideally get pb and b at the output, but b is not present. So i'm confused.

Can you please clarify.

View Image

Answer 1

The states {p, b} and {b} were represented by the state {p, b} in the product structure.

As you assumed, the states {b} and {b} would form a state {b} with no successors. It was however not shown in the solution.

Comments

That was super quick. Thanks Martin !! :)

But Product structures can have deadend states right ? So in that case if i draw b with no successors, the solution wouldn't go wrong ??

---

In fact, the correct product structure does include the deadend state with no incoming and no outgoing edge. There is actually an example like that in the lecture notes. However, the example solution of the exam decided to just sketch the product structure roughly to indicate that it was empty.

---

Well I would slightly disagree to that, as the lecture video had a state with no incoming and outgoing edges.

https://drive.google.com/file/d/1GRT3IgfLZGa0dzGnd_KgR6MjwyfWIiX9/view?usp=sharing

---

Why would you disagree to that? The slide you took the picture of was exactly the slide I talked about.

---

When you said this, " In fact, the correct product structure does include the deadend state with no incoming and no outgoing edge"

---

You can use the teaching tool http://es.cs.uni-kl.de/tools/teaching/BisimulationQuotients.html with the following inputs to see the full product structure (that includes a state {b} without ingoing and outgoing transitions):

vars p,a,b;
init 0,1;
labels 0:b; 1:a; 2:p,a; 3:p,b;
transitions 0->0; 0->1; 1->2; 1->3; 2->2; 2->3; 3->0;

vars a,b;
init 0,1;
labels 0:a,b; 1:; 2:a; 3:b;
transitions 0->1; 1->2; 1->3; 2->3; 3->0; 3->1;

---

I have added that state to the solutions of the mentioned exam paper.

---

Thank you Professor !

---

@mohan, yes, the sentence you quoted says nothing else than that this state is correct in the full solution. The slide I talked about was exactly the one I mentioned in the earlier comment. So you shouldn't slightly disagree but fully agree.