Propositional Dynamic Logic

The formal language of Propositional Dynamic Logic (PDL) is built up from two sets of primitive symbols, a countable set $At$ of atomic formulae and a countable set $Prg$ of atomic programs. The set of formulae is the least set containing $At$ and is closed under the rules: if $\alpha$ and $\beta$ are formulae then $\neg \alpha$ and $\alpha \to \beta$ are formulae; if $\alpha$ is a formula and $x$ is a program then $[x]\alpha$ is a formula. The set of programs is the least set containing all atomic programs and closed under the rule: if $x$ and $y$ are programs then $x;y$, $x\cup y$ and $x^*$ are programs; if $\alpha$ is a formula then ${\alpha}?$ is a program.

The dual operator to $[x]$ is defined as follows:

$$\langle x \rangle \alpha =_{def} \neg [x] \neg \alpha$$

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

• $x;y$: ``perform $x$ and then $y$'' (composition)

• $x\cup y$: ``do either $x$ or $y$'' (non-deterministic choice)

• $x^*$: ``perform $x$ finitely many (including zero) times'' (iteration)

• ${\alpha}?$: ``test if $\alpha$ currently holds''

• $[x]\alpha$: ``$\alpha$ always holds after $x$ is performed''

• $\langle x \rangle \alpha$: ``sometimes after $x$ is performed, $\alpha$ holds''.

A PDL-model is a structure $M=(W,R,V)$, where $W$ is a non-empty set, $R$ is a function which assigns to every program $x$ a binary relation $R(x)$ on $W$, and $V$ is a valuation function which assigns to every atomic formula $\phi$ a subset $V(\phi)$ of $W$.

The satisfaction relation ``$\alpha$ is true at point $s$ in model $M$'', denoted $M,s\models \alpha$, is defined inductively on the formation of $\alpha$ as follows:

1. $M,s\models \phi$ iff $s \in V(\phi)$ for any atomic formula $\phi$

2. $M,s \models \lnot \alpha$ iff $M,s\not\models \alpha$, i.e., it is not the case that $M,s\models \alpha$
3. $M,s \models \alpha \to \beta$ iff $M,s\not\models \alpha$ or $M,s \models \beta$

4. $M,s\models [x]\alpha$ iff for all $t\in W$, if $(s,t)\in R(x)$ then $M,s\models \alpha$

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

$$R(x;y)=R(x);R(y)$$

$$R(x\cup y)=R(x)\cup R(y)$$

$$R(x^*)=(R(x))^*$$

$$R({\alpha}?) = \{ (s,s) \in W \times W : M,s\models \alpha \}$$

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)

$[x]\alpha \land [x](\alpha \to \beta) \to [x]\beta$

(A2)

$[x;y]\alpha \leftrightarrow [x][y]\alpha$

(A3)

$[x \cup y]\alpha \leftrightarrow [x]\alpha \land [y]\alpha$

(A4)

$[x^*]\alpha \to \alpha \land [x]\alpha$

(A5)

$[x^*]\alpha \to [x^*][x^*]\alpha$

(A6)

$[x^*](\alpha \to [x]\alpha) \to (\alpha \to [x^*]\alpha)$

(A7)

$[{\alpha}?]\beta \leftrightarrow (\alpha \to \beta)$

(R1)

If $\alpha$ and $\alpha \to \beta$ are theorems, then $\beta$ is a theorem

(R2)

If $\alpha$ is a theorem, then so is $[x]\alpha$

It can be shown that the axiom (A5) is still valid if $R(x^+)=(R(x))^+$, i.e., if the program construct $x^*$ is interpreted by the transitive closure of the relation corresponding to $x$, and not by the reflexive, transitive one. This fact explains how the minimal temporal logic of transitive time K$_t$4 (with only the future operators) can be embedded into dynamic logic: the temporal operator ``always in the future'' is interpreted by the operator $[x^*]$, where $x$ is any (atomic) program.