Symbolic Representation of Kripke Structures

Question

Hello

Please may explain in below exam how do we compute the red highlighted part in "Problem 3.a"?

https://es.cs.uni-kl.de/teaching/vrs/exams/2021.02.17.vrs/2021.02.17.vrs.solutions.pdf

Comments

Also why from state {p} there is not a path to {q} since its transition relation result is p' XOR q' = (!p'&q') | (p'&!q')?

---

There is a transition missing from {p} to {q}, you are right, the figure has been fixed meanwhile.

---

Noted with thanks

Answer 1

You just consider the transition relation ((q⊕p′)∨(p∨q′))∧(p′⊕q′) and use the constant values, i.e.,

p=0 and q=0 : ((0⊕p′)∨(0∨q′))∧(p′⊕q′) = (p′∨q′)∧(p′⊕q′) = p′⊕q′
p=0 and q=1 : ((1⊕p′)∨(0∨q′))∧(p′⊕q′) = (!p′∨q′)∧(p′⊕q′) = (p'?0:q') = !p′∧q′
p=1 and q=0 : ((0⊕p′)∨(1∨q′))∧(p′⊕q′) = p′⊕q′
p=1 and q=1 : ((1⊕p′)∨(1∨q′))∧(p′⊕q′) = p′⊕q′

Comments

Hello, can you please explain the first two lines? I could not understand how these happens.

(p′∨q′)∧(p′⊕q′) = p′⊕q′

(!p′∨q′)∧(p′⊕q′) = (p'?0:q') = !p′∧q′

---

(p′∨q′)∧(p′⊕q′) = p′⊕q′ holds since the satisfying assignments of p′⊕q′ are contained in the satisfying assignments of p′∨q′ (which has the additional one where both p′ and q′ are true). Hence, the intersection of both is just the set of satisfying assignments of p′⊕q′

For, (!p′∨q′)∧(p′⊕q′) = (p'?0:q'), we made a case distinction, i.e., Shannon decomposition on p': If p' is true, then we have (!1∨q′)∧(1⊕q′) which is q′∧(1⊕q′), i.e., q′∧!q′, thus 0. If p' is false, we get (!0∨q′)∧(0⊕q′) which is (1∨q′)∧(0⊕q′) = 1∧q′ = q′.