Dynamic Logic (modal Logic) - Propositional Dynamic Logic (PDL)

Propositional Dynamic Logic (PDL)

Ordinary or first-order logic has two types of terms, respectively assertions and data. As can be seen from the examples above, dynamic logic adds a third type of term denoting actions. The dynamic logic assertion contains all three types:, and are data, is an action, and and are assertions. Propositional logic is derived from first-order logic by omitting data terms and reasons only about abstract propositions, which may be simple propositional variables or atoms or compound propositions built with such logical connectives as and, or, and not.

Propositional dynamic logic, or PDL, was derived from dynamic logic in 1977 by Michael J. Fischer and Richard Ladner. PDL blends the ideas behind propositional logic and dynamic logic by adding actions while omitting data; hence the terms of PDL are actions and propositions. The TV example above is expressed in PDL whereas the next example involving is in first-order DL. PDL is to (first-order) dynamic logic as propositional logic is to first-order logic.

Fischer and Ladner showed in their 1977 paper that PDL satisfiability was of computational complexity at most nondeterministic exponential time, and at least deterministic exponential time in the worst case. This gap was closed in 1978 by Vaughan Pratt who showed that PDL was decidable in deterministic exponential time. In 1977, Krister Segerberg proposed a complete axiomatization of PDL, namely any complete axiomatization of modal logic K together with axioms A1-A6 as given above. Completeness proofs for Segerberg's axioms were found by Gabbay (unpublished note), Parikh (1978), Pratt (1979), and Kozen and Parikh (1981).