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](http://plato.stanford.edu/entries/logic-dynamic/ "Propositional dynamic logic").


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.



Applications of propositional dynamic logic
The practical applications might be more obvious once you observe that these propositional "programs" are *regular expressions* -- which is to say, state machines. So you can expect it to have applications in the study of things [like program analyses](http://www.cs.cornell.edu/~kozen/papers/opti.pdf) and verifying concurrent protocols.


[Dexter Kozen](http://www.cs.cornell.edu/~kozen/papers/papers_expanded.htm) at Cornell has done a great deal of work in this area. In fact, he's mostly focused on a subsystem of PDL, called ["Kleene algebra with tests"](http://www.cs.cornell.edu/~kozen/papers/kat.ps), which has an easier decision problem (PSPACE rather than EXPTIME) and tends to have nicer equational proofs. 


