Exam August 2020 problem 7

Question

Hi,

Is my solution correct?

EDIT: Correct Solution as instructed by Professor and Martin.

Answer 1

I think that your solution is not correct. The formulas are both satisfied in the initial state of your structure. I quickly checked it with the model checker and got the following for S2:

The tool then computed 

〖!(a & c <-> d & c)〗= {s1;s3;s4;s6}

〖A G !(a & c <-> d & c) | [] Z〗 = {s3;s6}

〖A X A F A G !(a & c <-> d & c)〗 = {s0;s1;s2;s3;s4;s5;s6}

Comments

could you please share the input to the tool which you have given to check the solution? I don't know how to write the path from S0 to these two states.

---

Sorry, I already removed it. But you just have to add the following transitions

0->1; 1->2; 2->3; 3->3;
0->4; 4->5; 5->6; 6->6;

The labels are clear, I guess.

---

Both formulas start with AX. So we just look at the left most non-initial states and the paths from there. The paths starting from these two states are indistinguishable. Hence, you can delete one of the two parallel paths.
Now, you are just left with one path. However, the difference between the two formulas is the A-quantifier. Since you only have one path, “all paths from here” and “the paths you are on from here” are the same.

---

Thanks Professor,
Great insight Martin, I know where the Mistake is thanks

---

Feel free to add your corrected solution.

---

It will be a nice example for minimizing the transition system by bisimulation relations.

---

@Martin Correct Solution added.

---

Beautiful! Thanks

---

I think the updated solution is also not correct:〖A X A F A G !(a & c <-> d & c))〗 = {s0;s1;s2;s3}, and〖A F G !(a & c <-> d & c))〗 = {s0;s1;s2;s3}, thus also〖A X A F G !(a & c <-> d & c))〗 = {s0;s1;s2;s3}. Hence, both formulas are satisfied with this structure as before. I think you have to switch the labels from {) to {a,c} and vice versa. Am I wrong?

---

Oh but from the tool i checked that property A X A F A G !(a & c <-> d & c) holds in states {s2;s3}. Other thing is that its just NOT the minimization, because I have added one transition from s1, ->s1 as well.Hence its not equivelant

---

You are right. I missed the self-loop on s1. Then, it's correct, I agree. Since then A X A F A G !(a & c <-> d & c) holds in states {s2;s3} as you said, and A X A F G !(a & c <-> d & c) holds in all states, i.e., in particular in s0.