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


Is my solution correct?

EDIT: Correct Solution as instructed by Professor and Martin.

in * TF "Emb. Sys. and Rob." by (1.4k points)
edited by

1 Answer

+1 vote
Best answer

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}

by (166k points)
selected by
@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.

Related questions

0 votes
1 answer
asked Jan 26, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by Nicola (800 points)
Imprint | Privacy Policy