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	Name	Meaning
[ ]	—	Square brackets	Box modality: after every execution, φ
⟨ ⟩	U+27E8, U+27E9	Mathematical angle brackets	Diamond modality: after some execution, φ
;	U+003B	Semicolon	Sequential composition
*	—	Kleene star	Finite iteration, zero or more times
∪	U+222A	Union	Nondeterministic choice of programs
?	—	Question mark	Test: filter on states satisfying a formula
∘	U+2218	Ring operator	Relational composition, the semantics of ;
⊨	U+22A8	True	Satisfaction at a world of a Kripke structure
π, ρ	U+03C0, U+03C1	Greek small pi, rho	Program metavariables
α, β	U+03B1, U+03B2	Greek small alpha, beta	Atomic programs
φ, ψ	U+03C6, U+03C8	Greek small phi, psi	Schematic formulas
R_π	—	Transition relation	Interpretation of the program π
::=	—	Production	Grammar clause of the syntax
¬	U+00AC	Not sign	Negation
∧	U+2227	Logical and	Conjunction
→	U+2192	Rightwards arrow	Material implication
↔	U+2194	Left right arrow	Material equivalence, as in the reduction axioms
∀, ∃	U+2200, U+2203	For all, there exists	Quantifiers in the truth clauses
ν	U+03BD	Greek small nu	Greatest fixed point of the μ-calculus translation
Π¹₁	—	Pi-one-one	Analytical class of context-free PDL validity
M, w	—	Model, world	Point of evaluation

Metatheory. Fischer and Ladner (1979) proved the small model property by way of the closure that bears their name: a satisfiable formula has a model of size at most exponential in the formula, which gives decidability, and Pratt supplied the exponential-time decision procedure. Satisfiability is EXPTIME-complete, the lower bound by reduction from alternating polynomial-space Turing machines. The axiomatization — K for every program modality, the reduction axioms for composition, choice and test, the fixed-point axiom [π*]φ ↔ φ ∧ [π][π*]φ, and the induction axiom — was conjectured by Segerberg (1977) and proved complete by Parikh, and later by Kozen and Parikh (1981) with a shorter argument. PDL is invariant under bisimulation and translates into the modal μ-calculus, where the star is the greatest fixed point νX.(φ ∧ [π]X); the inclusion is proper, since μ-calculus alternation is not available in PDL. Model checking is polynomial in the structure and the formula.

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

Limitations. Programs are regular expressions, so recursive procedures are outside the language, and admitting them is not a mild extension: PDL over context-free programs is Π¹₁-complete, hence not even arithmetical, a result of Harel, Pnueli, and Stavi (1983). PDL is not compact — the set {⟨a*⟩p} ∪ {¬p, ¬⟨a⟩p, ¬⟨a;a⟩p, …} is finitely satisfiable and unsatisfiable — so the axiomatization is weakly and not strongly complete, and no finitary proof system can be strongly complete. Adding intersection of programs preserves decidability but raises satisfiability to 2EXPTIME-complete (Lange and Lutz 2005); adding program complement loses decidability. Being propositional, it cannot quantify over data, and first-order dynamic logic over the naturals is not recursively enumerable. Being bisimulation-invariant, it cannot distinguish bisimilar structures and cannot state any property relating two executions.