PDL Extensions

Origin. Various (1980s-present). Test-free, deterministic, concurrent PDL. Process logics. Beyond basic PDL. Rich program logics.

Models. Various extensions of propositional dynamic logic. Different program constructs. Different expressivity/decidability tradeoffs. Program reasoning.

Formalism.

Concurrent PDL (CPDL): α ∩ β: concurrent execution. Both α and β simultaneously. Intersection of programs. More expressive.

Deterministic PDL (DPDL): All programs deterministic. ⟨α⟩φ → [α]φ always holds. Functional accessibility. Different complexity.

Test-free PDL: No φ? tests. Only basic programs, ;, ∪, *. Still expressive. Simpler semantics.

PDL with converse: α⁻: backward execution. Undo program α. Past reasoning. ⟨α⁻⟩φ: was φ before α.

Game PDL: Programs as games. Player and opponent moves. Game logic ⊂ PDL(∩). Strategic reasoning.

Looping programs: α^ω: infinite iteration. Fairness conditions. Büchi-like acceptance. Beyond finite behavior.

Complexity variations: PDL: EXPTIME-complete. CPDL: EXPTIME-complete. PDL + nominals: can be undecidable. Careful extension design.

Symbols.

Symbol	Unicode	Meaning
∩	U+2229	concurrent composition
α⁻	—	converse program
α^ω	—	infinite iteration
CPDL	—	concurrent PDL

Metatheory. Program logic extensions. Expressivity. Decidability. Completeness.

Applies to. Program verification. Game theory. Action logic. Concurrent systems.

Limitations. Complexity increases. Extension compatibility. Semantic complexity. Limited tools.