 Following earlier approaches to reason about programs in Engeler (1967) and Hoare (1969), Propositional dynamic logic (PDL), the logic of programs (Harel, Kozen, &amp; Tiuryn 2000), intends to describe what programs can achieve. Semantically, programs are interpreted in standard relational models, with one binary relation \(R_a\) for every basic program a; syntactically, the language contains a modality \([a]\) for each such a.