Dynamic Logic

Origin. Vaughan Pratt introduced dynamic logic in 1976 ("Semantical considerations on Floyd–Hoare logic"), reading programs as modalities. Fischer and Ladner isolated the propositional fragment PDL, combining modal logic with regular expressions over programs, and settled its complexity (1977, 1979). David Harel developed the first-order theory (1979). 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. Fischer and Ladner (1979) proved the small model property — every satisfiable formula has a model exponential in its length, so PDL has the finite model property — and established the EXPTIME lower bound; Pratt's tableau construction supplies the matching upper bound, making PDL satisfiability EXPTIME-complete. Segerberg (1977) proposed the axiomatization, whose distinctive component is the induction axiom [α*](φ → [α]φ) → (φ → [α*]φ), and Parikh (1978) proved it complete for the Kripke semantics. Completeness is weak only, since PDL is not compact: ⟨a*⟩p together with ¬p, ¬⟨a⟩p, ¬⟨a;a⟩p and so on is finitely satisfiable but has no model. PDL translates faithfully into the modal μ-calculus and is properly weaker, the μ-calculus expressing fixpoints no regular program describes. First-order dynamic logic is not recursively enumerable — its validities are Π¹₁-complete — so it admits no finitary complete axiomatization.

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's programs are regular, so non-regular control — recursion, or a procedure that executes α some number of times and then β the same number — is inexpressible, and adding it destroys decidability outright: Harel, Pnueli and Stavi showed PDL with context-free programs to be Π¹₁-complete. The box is vacuously true when α fails to terminate, so [α]φ expresses partial correctness only and total correctness must be stated separately as ⟨α⟩φ. There is no program constructor for parallel composition, so concurrency has to be encoded as interleaving by hand. The decidability that makes PDL attractive does not survive the addition of data: first-order dynamic logic, the level at which actual programs live, is Π¹₁-complete and admits no complete finitary proof system, so mechanization there rests on relative completeness with respect to an arithmetical oracle.

© 2026 Lingenic LLC