Propositional dynamic logic (PDL) is an example of a (multi)modal logic with a structure on the set of modalities. In particular, the set of its modalities is indexed by "programs" and one can use program constructors such as composition, choice and iteration to make new programs out of old (of course, there is a set of basic programs to begin with). So if π and ρ are programs, so are π;ρ, π∪ρ and ρ*. The intuitive interpretations are, respectively, "run π, then run ρ", "nondeterministically run either π or ρ", and "run ρ finite number of times".

The formulas in this language are formed from propositional letters using boolean connectives. Also, if π is a program and φ a formula, then <π>φ is a formula with intuitive interpretation "there is a state of computation accessible by program π in which φ is satisfied". Modality <π> is read "diamond π".

Not to dwell any deeper right now, I refer you to a very well written article about PDL.

Now to get to my question. PDL was created in a line of formal systems that were ment to be used to "talk about" programs, prove program correctness etc. Its predecessors were Hoare logic (HL, also known as Floyd-Hoare logic) and its modal version, the dynamic logic (DL). But, since PDL is propositional, it lacks the expressiveness given by first-order constructions found in HL and DL. So, somehow I haven't really been able to find any real example of its original use.

Does anyone know an example of a program and its specifications that I can express and verify for correctness in PDL? I would be happy with any academic or real-world example, or any reference of such an example.

I would even be happy with an example of use of PDL in other areas. Most books that I've seen mention its use in philosophy, artificial intelligence, linguistics etc., but never give an example of this use.