Global Model Checking

Question

Hello all,

Exam February 19th, 2020 ,  problem 4 in step 0 why we did not find the following :

[a]= s0,s2 ,s3, s4 , s6 , s7

[b]=s4,s5

aVb = s0,s2,s3,s4,s5,s6,s7

aVb & <> x= s0,s2,s3,s4,s5,s6

Answer 1

Recall the precedence rules (that you find in the propositional logic chapter): conjunction binds stronger than disjunction, hence, a ∨ b ∧ <>x is to be read as a ∨ (b ∧ <>x) and not as (a ∨ b) ∧ <>x.

Comments

Alright , I got it , thank you.
But still I need help as I am not getting the exact answer as the exam paper, here how I solved it :
step 0 :
x={s0,s1,s2,s3,s4,s5,s6,s7}
<>x={ s0,s1, s2,s3,s4,s5,s6}
[b]=s4,s5
b & <>x= s4,s5
[a]=s0,s2,s3,s4,s6,s7
a V (b& <>x)=s0,s2,s3,s4,s5,s6,s7
step 1:
x=s0,s2,s3,s4,s5,s6,s7
<>x=s0,s1,s2,s3,s4,s5,s6
b & <>x =s4,s5
a V (b & <>x) = s0 , s2 , s3 , s4 , s5 , s6 , s7
fixpoint reached

---

Well, if you compare your solution with the example solution for the exam, you see just one difference: Instead of States(b) = {s0;s4;s5}, you have States(b) = {s4;s5}, but that does not matter since the final union with States(a) = {s0;s2;s3;s4;s6;s7} adds back state s0. Apart from this, and the consequence that you also got States(b&<>x) = {s4;s5} instead of States(b&<>x) = {s0;s4;s5}, everything seems to be right.

---

Thank you so much .