In Krister Segerberg’s modal logic seminar here in Calgary, we were talking about propositional dynamic logic last week. PDL was originally introduced (by Vaughn Pratt in the early 70’s) to reason about programs. In the language, you have propositional variables but then also variables for (indeterministic) programs. Moreover, you have complex terms for programs, e.g., if α and β are programs then α ∪ β is “either do α or do β”, α;β is “first do α then do β”, α* is “do α 0 or more times. If α is a program term and φ is a formula, then [α]φ means “after every execution of α, φ is true”.
The semantics for PDL is your regular Kripke semantics where W is a set of states, V maps propositional variables into ℘(W), and R maps program variables into ℘(W2). The idea is that V(φ) is the set of states where φ holds, and v R(α) w if α takes you from state w to state v (α may be nondeterministic, so it’s a relation, not a function). The definition of ||- is as you’d expect, with w ||- [α]φ if v ||- φ for all v so that w R(α) v. You can put in program constants, e.g., the program 0 that just freezes (R(0) = ∅), the program 1 that does nothing and immediately halts (R(1) = ΔW), and the completely indeterministic program that can take you to any state from any state (R(U) = W2).
Most of the people in the seminar are philosophers, not computer scientists, so we were talking a fair amount of time about how to interpret this semantics not in terms of programs. One way to think of the α’s is as actions types: α is an action type, [α]φ means “φ is true after every action of type α”, and w R(α) v if some action of type α can take you from w to v. For instance, think of W as the set of chess configurations (together with whether it’s black’s or white’s move). Then α might be “move the king”. But this is still pretty close to the programs-changing-state interpretation.
I was thinking of a completely different interpretation, and was wondering if anyone has thought about this interpretation and if it might have any use: In the “intended” interpretation, R(α) tells you which states you can get to from a given state by doing α. But R(α) may be seen as an ordinary modal accessibility relation on W. On this interpretation, PDL turns into a parametrized multi-modal logic with operations on modalities: α is an accessibility relation (e.g., U is the total relation–every world is accessible from every world), [α]φ means “φ is α-necessary), and the operations on programs turn into operations on accessibility relations, e.g., 1 ∪ α is the reflexive closure of α and α* is the transitive closure of α. My hunch is that, maybe by adding some additional operations on the α’s, this could make PDL into a logic of modalities in general.