DYNAMIC LOGIC
Logics whose modalities are indexed by actions, programs, or transitions, so that [α]φ reads "after every execution of α, φ holds." Meaning is given over labelled transition systems and the algebra of actions, making these the modal logics of change and computation.
Entries are organized around three themes. Program modalities—propositional dynamic logic and its many extensions—form the core. The algebra of actions is captured by Kleene algebra and arrow logic. Expressive extensions add fixed points and games: the modal μ-calculus in its PDL setting, game logic, sabotage logic, and the spatial and mereotopological logics that treat regions and their transformations.