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 ∧