 To give meaning to statements in PDL, we typically work with an abstract semantics in terms of Labeled Transition Systems (LTS). LTSs can be seen as a generalization of Kripke models, where transitions between worlds, or states, are “labeled” by names of atomic programs. A valuation indicates for every state what propositions are true in it. A transition labeled π from one state x to a state y—noted xR(π)y, or (x,y) ∈ R(π)—indicates that starting in x, there is a possible execution of the program π that finishes in y. If the proposition A is true in y, then the formula &lt;π&gt;A is true in x: i.e., in the state x there is a possible execution of the program α that ends in a state satisfying A. One recognizes in &lt;π&gt; a modality reminiscent of the modality of possibility (often noted ◊) of modal logic. Unsurprisingly, there is also a corresponding notion of necessity (whose modality is often noted □). The formula [π]A will be true in the state x if A is true in every state reachable from x by a transition labeled π. 