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

@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.