Dynamic Logic

Origin. Vaughan Pratt introduced Propositional Dynamic Logic (PDL) in 1976, combining modal logic with regular expressions over programs. David Harel extended it to first-order (1979). Fischer and Ladner analyzed complexity. Foundational for program verification and reasoning about actions.

Models. Programs as modalities. What is true after executing a program? A program transforms states; [α]φ means "after every execution of α, φ holds." Combines reasoning about necessity (modal logic) with reasoning about actions (program semantics). Programs are first-class objects with compositional structure.

Formalism.

Propositional Dynamic Logic (PDL):

Programs (α, β, ...):

• Atomic programs: a, b, c, ...
• Composition: α;β (do α then β)
• Choice: α ∪ β (do α or β nondeterministically)
• Iteration: α* (do α zero or more times)
• Test: φ? (proceed if φ true, fail otherwise)

Formulas:

• Propositional atoms: p, q, r, ...
• Boolean connectives: ¬, ∧, ∨, →
• Box modality: [α]φ (after every execution of α, φ holds)
• Diamond modality: ⟨α⟩φ (after some execution of α, φ holds)

Semantics: Kripke structures (W, {Rα}, V) where Rα ⊆ W × W is the accessibility relation for program α.

• R_{α;β} = Rα ∘ Rβ (composition)
• R_{α∪β} = Rα ∪ Rβ (union)
• R_{α*} = (Rα)* (reflexive transitive closure)
• R_{φ?} = {(w,w) | w ⊨ φ} (identity on φ-states)

Truth: w ⊨ [α]φ iff for all v, wRαv implies v ⊨ φ.

First-Order Dynamic Logic: Adds quantifiers, function symbols, assignment programs (x := e), loops, conditionals.

Symbols.

Metatheory. PDL is decidable (EXPTIME-complete). First-order dynamic logic is not recursively enumerable (highly undecidable). PDL is complete with respect to its Kripke semantics. The test construct gives PDL the power of propositional logic embedded in programs. Segerberg's axioms axiomatize PDL. Regular programs (PDL) capture exactly the regular languages; extensions (looping constructs, recursion) increase power.

Applies to. Program verification (partial and total correctness). Hoare logic embedded in dynamic logic: {P}α{Q} as P → [α]Q. Action logic in AI. Game logic (players as programs). Database updates. Security protocols.

Limitations. PDL cannot express all program properties — only regular properties. Recursion requires extensions (μ-calculus, Game Logic). First-order dynamic logic is undecidable, limiting automation. No native treatment of concurrency (see process algebra). The semantics assumes termination for [α]φ to be vacuously true on non-termination, which may not match intuitions. Expressing real programs requires bridging the gap between PDL's abstract programs and actual code.

© 2026 Lingenic LLC