Informally, the mapping R assigns to each atomic program π ∈ Π0 some binary relation R(π) on W with intended meaning xR(π)y iff there exists an execution of π from x that leads to y, whereas the mapping V assigns to each atomic formula p ∈ Φ0 some subset V(p) of W with intended meaning x ∈ V(p) iff p is true in x. Given our readings of 0, ¬A, A∨B, [α]A, α;β, α∪β, α* and A?, it is clear that R and V must be extended inductively as follows to supply the intended meanings for the complex programs and formulas: