Thank you. But in one of the exercise solution pdf, it was written that "In successor we rename (p, q, a) to (p′, q′, a′) and vice-versa ".
Example solved in the solution sheet of the exercise
Let each state in the Kripke structure be described by the variables {p, q, a, o}.
Let the transition relation R be described by ψR = (p′ ↔ q) ∨ a. Let the set Q be described by φQ = ¬p
suc∀R(Q) = {s2 | ∀s1(s1,s2) ∈ R → s1 ∈ Q}
suc∀R(Q) = ∀p′,q′,a′ [(p ↔ q′) ∨ a′) → ¬p′]
(In successor we rename (p, q, a) to (p′, q′, a′) and vice-versa )
=[1]p′=0 ∧[¬((p↔q′)∨a′)]p′=1
=[¬((¬p)∨a′)]q′=0 ∧[¬((p)∨a′)]q′=1
= [1]a′=0 ∧ [0]a′=1
= 0/ false
Note:For universal ∀, the separator is ∧
