Formulas can be used to describe the properties that hold after the successful execution of a program. For example, the formula [α∪β]A means that whenever program α or β is successfully executed, a state is reached where A holds, whereas the formula &lt;(α;β)*&gt;A means that there is a sequence of alternating executions of α and β such that a state is reached where A holds. Semantically speaking, formulas are interpreted by sets of states and programs are interpreted by binary relations over states in a transition system. More precisely, the meaning of PDL formulas and programs is interpreted over Labeled Transition Systems (LTS) M = (W, R,V) where W is a nonempty set of worlds or states, R is a mapping from the set Π0 of atomic programs into binary relations on W and V is a mapping from the set Φ0 of atomic formulas into subsets of W.