Next: Formal Proofs Up: Propositional modal, temporal, and Previous: Basic temporal logic   Contents

# Propositional Dynamic Logic

The formal language of Propositional Dynamic Logic (PDL) is built up from two sets of primitive symbols, a countable set of atomic formulae and a countable set of atomic programs. The set of formulae is the least set containing and is closed under the rules: if and are formulae then and are formulae; if is a formula and is a program then is a formula. The set of programs is the least set containing all atomic programs and closed under the rule: if and are programs then , and are programs; if is a formula then is a program.

The dual operator to is defined as follows:

The intuitive reading of the program connectives and the formulae are as follows:

• : perform and then '' (composition)

• : do either or '' (non-deterministic choice)

• : perform finitely many (including zero) times'' (iteration)

• : test if currently holds''

• :  always holds after is performed''

• : sometimes after is performed, holds''.

A PDL-model is a structure , where is a non-empty set, is a function which assigns to every program a binary relation on , and is a valuation function which assigns to every atomic formula a subset of .

The satisfaction relation  is true at point in model '', denoted , is defined inductively on the formation of as follows:

1. iff for any atomic formula

2. iff , i.e., it is not the case that
3. iff or

4. iff for all , if then

To preserve the intuitive reading of the program connectives, the following formal requirements must be met:

Well-known results say that PDL is decidable and finitely axiomatizable (cf. [Har84], [Gol87], [KT90]). A complete axiomatization consists of the following axioms and inference rules:

(A0)
All propositional tautologies

(A1)

(A2)

(A3)

(A4)

(A5)

(A6)

(A7)

(R1)
If and are theorems, then is a theorem

(R2)
If is a theorem, then so is

It can be shown that the axiom (A5) is still valid if , i.e., if the program construct is interpreted by the transitive closure of the relation corresponding to , and not by the reflexive, transitive one. This fact explains how the minimal temporal logic of transitive time K4 (with only the future operators) can be embedded into dynamic logic: the temporal operator always in the future'' is interpreted by the operator , where is any (atomic) program.

Next: Formal Proofs Up: Propositional modal, temporal, and Previous: Basic temporal logic   Contents
2001-04-05