PDL Extensions

Origin. The family grew from Fischer and Ladner's PDL (1979) as researchers asked which program constructors could be added without losing decidability. Ben-Ari, Halpern and Pnueli (1982) settled deterministic PDL; Berman and Paterson (1981) proved tests are not eliminable; Streett (1982) handled looping and converse; Harel, Pnueli and Stavi (1983) showed where non-regular programs lead; Lange and Lutz (2005) fixed the cost of intersection. Parikh's game logic (1985) is the branch in which a second player appears.

Models. One question organizes the family: which additions to the regular program constructors preserve the exponential-model property that makes PDL decidable. Each extension names a program constructor, and the interesting cases are those where the constructor is not definable from the others yet leaves satisfiability decidable — usually at a higher cost. The boundary is sharp: intersection costs an exponential, converse is free, and non-regular control is not merely undecidable but analytically hard.

Formalism.

PDL with intersection (IPDL): α ∩ β: the transition relation is Rα ∩ Rβ. A run counting as both an α-run and a β-run. Not definable from ;, ∪, * and ?. Note this is intersection of relations, not parallel execution: genuine concurrency needs a separate constructor.

Deterministic PDL (DPDL): Every atomic program interpreted as a partial function. ⟨α⟩φ → [α]φ holds for every α. Functional accessibility; the frame class is restricted, not the language.

Test-free PDL: No φ? tests. Only atomic programs, ;, ∪, *. Properly less expressive than PDL (Berman–Paterson 1981): tests cannot be simulated by the other constructors.

PDL with converse: α⁻: R_{α⁻} = (Rα)⁻¹. Backward execution; past reasoning. ⟨α⁻⟩φ: φ held at some state from which α leads here.

Game PDL: Programs as games. Player and opponent moves. ∪ is angelic choice, ∩ demonic; Parikh's game logic adds a dual operator that PDL with intersection does not have. Strategic reasoning.

Looping and repeat: Δα (repeat): α admits an infinite computation from here. α^ω: infinite iteration; Büchi-style acceptance. Not expressible in PDL, whose star is finite iteration.

Non-regular programs: Context-free program schemes, e.g. aⁿ;b;cⁿ. Beyond the regular languages the star generates.

Complexity variations: PDL: EXPTIME-complete. PDL with converse: EXPTIME-complete. Deterministic PDL: EXPTIME-complete. PDL with looping and converse: elementarily decidable (Streett 1982); EXPTIME-complete (Vardi–Stockmeyer 1985). PDL with intersection: 2EXPTIME-complete (Lange–Lutz 2005). PDL with context-free programs: Π¹₁-complete (Harel–Pnueli–Stavi 1983).

Symbols.

Metatheory. The family is a map of where decidability breaks. Converse adds nothing: PDL with converse remains EXPTIME-complete, and Streett (1982) showed that adding the repeat construct as well keeps it elementarily decidable, with Vardi and Stockmeyer (1985) bringing the bound down to EXPTIME. Determinism does not help either way — DPDL is also EXPTIME-complete (Ben-Ari, Halpern and Pnueli 1982) — and tests, though not eliminable, do not affect the class, since Fischer and Ladner's lower bound already applies to the test-free fragment while Berman and Paterson (1981) proved test-free PDL properly less expressive. Intersection is the first genuine cost: satisfiability rises to 2EXPTIME-complete (Lange and Lutz 2005), because ∩ destroys the tree model property that the automata constructions rely on. Beyond the regular programs the collapse is total: PDL with context-free programs is Π¹₁-complete (Harel, Pnueli and Stavi 1983), not merely undecidable but outside the arithmetical hierarchy.

Applies to. Program verification where the base logic is too weak. Description logic, whose expressive members are PDL variants with converse and nominals. Epistemic and action logics needing a past operator. Comparative study of where decidability fails. Game logic, as the branch with a second player.

Limitations. The extensions do not compose: each is decidable on its own, but combining features can be undecidable even when no single one is, and there is no general theorem saying which combinations survive. The closest precise statement is for the μ-calculus, where nominals, inverse programs and graded modalities together give undecidability while dropping any one of the three restores EXPTIME. Intersection is the informative case for why: ∩ destroys the tree model property, so the automata-theoretic method that gives every other extension its EXPTIME bound has to be replaced rather than adapted, and the exponential is not an artifact. None of these logics is closed under the constructor it lacks — the concurrency that ∩ is often read as providing is intersection of relations and not parallel execution, and no PDL variant has a genuine parallel constructor with a decidable theory.

© 2026 Lingenic LLC