Propositional Dynamic Logic

Origin. Fischer and Ladner introduced PDL (1979). Modal logic of programs. Combines propositional logic with regular expressions over actions. Foundation for program verification. Decidable fragment of dynamic logic.

Models. Programs as modalities. Actions: atomic programs α, β. Compound: α;β (sequence), α∪β (choice), α* (iteration), φ? (test). [α]φ: after all executions of α, φ holds. ⟨α⟩φ: after some execution, φ holds.

Formalism.

Programs: π ::= a | π;π | π∪π | π* | φ?

Formulas: φ ::= p | ¬φ | φ∧ψ | [π]φ | ⟨π⟩φ

Semantics (Kripke structure with relations Rₐ for each a):

R_{π;ρ} = R_π ∘ R_ρ (sequential composition)
R_{π∪ρ} = R_π ∪ R_ρ (choice)
R_{π*} = R_π* (reflexive transitive closure)
R_{φ?} = {(w,w) : w ⊨ φ} (test)

M, w ⊨ [π]φ iff ∀v. wR_π v → M, v ⊨ φ M, w ⊨ ⟨π⟩φ iff ∃v. wR_π v ∧ M, v ⊨ φ

Key validities:

π → ([π]φ→[π]ψ)
[π;ρ]φ ↔ [π][ρ]φ
[π∪ρ]φ ↔ [π]φ ∧ [ρ]φ
[π*]φ ↔ φ ∧ [π][π*]φ
[φ?]ψ ↔ (φ→ψ)

Induction axiom: φ ∧ π* → [π*]φ

Symbols.

Symbol	Unicode	Meaning
[α]φ	—	box modality
⟨α⟩φ	—	diamond modality
;	—	sequential composition
*	—	iteration

Metatheory. PDL is decidable (EXPTIME-complete). Finite model property. Complete axiomatization with induction rule. Bisimulation invariant. Strictly less expressive than first-order dynamic logic. Extends to ΔPDL, GPDL with more operators.

Applies to. Program verification. Action languages in AI. Workflow modeling. Protocol analysis. Game descriptions. Access control policies. Agent programming.

Limitations. Only regular programs (no recursion beyond iteration). No first-order quantification. Cannot express some program properties. Recursion requires extensions (μ-calculus). EXPTIME complexity may be high for large formulas.