Kripke Structure to Büchi automata

Consider a Kripke Structure K = (AP, W, W0, R, l). We construct an NBA AK such that AK accepts a computation $\pi \in (2^{AP}{)}^{\omega }$ iff π is a computation of K. The construction of AK essentially moves the labels of K from the states to the transitions. Thus, AK = $(2^{AP},W,W0,\delta ,W)$, where for all w ∈ W and σ ∈ $2^{AP}$, we have:

if $\sigma =l(w)$ then

$\delta (w,\sigma )=\{w^{\prime }:R(w,w^{\prime })\}$

else $\delta (w,\sigma )=\varnothing$