# Propositional Dynamic Logic

*First published Thu Feb 1, 2007; substantive revision Tue Jul 3, 2007*

Logics of programs are modal logics arising from the idea of associating with each computer program α of a programming language a modality [α]. This idea stems from the works of Engeler [1967], Hoare [1969] and Yanov [1959] who formulated and studied logical languages in which the properties of program connectives can be expressed. The algorithmic logic (AL) developed by Salwicki [1970] and the dynamic logic (DL) elaborated by Pratt [1976] are proper continuations of these works. The numerous papers devoted to AL, DL and their variants as well as their multifarious applications in program verification and data structures show that these logics constitute useful tools in studying properties of programs. Concerning AL, not described here, the reader is invited to consult the work studied in Mirkowska and Salwicki [1987]. Concerning DL, Pratt chose to depict his work on what one might call the first-order level, but it was his work that triggered Fisher and Ladner to define the propositional variant of DL a couple of years later. This article presents an introduction to PDL, the propositional variant of DL, where primitive programs are interpreted as binary relations on an abstract set of states.

## 1. Introduction

Propositional dynamic logic (PDL) was first defined by Fischer and
Ladner [1979]. It is based on Pratt's idea of associating with each
computer program α of a programming language a modality
[α], the formula [α]*A* being read “whenever
program α terminates, it must do so in a state satisfying
formula *A*”. Syntactically, PDL is a modal logic with an
algebraic structure in the set of modalities: composition
α;β of programs α and β corresponds to the
composition of the accessibility relations *R*(α) and
*R*(β), test *A*? on formula *A* corresponds
to the partial identity relation on sets of states in which the
formula *A* is true, union α∪β of programs
α and β corresponds to the union of the accessibility
relations *R*(α) and *R*(β), and iteration
α* of program α corresponds to the reflexive and
transitive closure of the accessibility relation
*R*(α). At the most intuitive level, an intended
interpretation of these operations is as follows: executing
composition α;β means “first do α and then do
β”, executing test *A*? means “if *A* then skip
else abort”, executing union α∪β means “do α or
do β nondeterministically”, executing iteration α* means
“repeat α a finite number of times”. There are by now a number
of books—Goldblatt [1982], Goldblatt [1992], Harel [1979] and
Harel et al. [2000]—and survey papers—Harel [1984], Kozen
and Tiuryn [1990] and Parikh [1983]—treating PDL and a great
deal is known concerning its complexity and its proof theory: it is
shown in Pratt [1980] how the satisfiability problem for PDL can be
solved in deterministic exponential-time whereas an elementary proof
of the completeness of the deductive system formulated by Segerberg
[1977] is given in Kozen and Parikh [1981]. Additional topics related
to PDL include results concerning comparative power of expression,
decidability, complexity and completeness of a number of interesting
variants obtained by extending or restricting PDL in various ways:
deterministic programs, restricted tests, nonregular programs,
programs as automata, complementation and intersection of programs,
converse and infinite computations, etc. We devote this article to the
study of the syntax and semantics of PDL
(section 2),
axiomatization and completeness
(section 3),
decidability and complexity
(section 4),
and variants of PDL
(section 5).

## 2. Syntax and semantics

Propositional dynamic logic (PDL) is designed for representing and
reasoning about propositional properties of programs. Its syntax is
based upon two sets of symbols: a countable set Φ_{0} of
atomic formulas and a countable set Π_{0} of atomic
programs. Complex formulas and complex programs over this base are
defined as follows:

- Every atomic formula is a formula
- 0 (“false”) is a formula
- If
*A*is a formula then ¬*A*(“not*A*”) is a formula - If
*A*and*B*are formulas then (*A*∨*B*) (“*A*or*B*”) is a formula - If α is a program and
*A*is a formula then [α]*A*(“every execution of α from the present state leads to a state where*A*is true”) is a formula - Every atomic program is a program
- If α and β are programs then (α;β) (“do α followed by β”) is a program
- If α and β are programs then (α∪β) (“do α or β, nondeterministically”) is a program,
- If α is a program then α* (“repeat α a finite, but nondeterministically determined, number of times”) is a program.
- If
*A*is a formula then*A*? (“proceed if*A*is true, else fail”) is a program

The other Boolean connectives 1,
∧
and → are used as abbreviations in the standard way. In
addition, we abbreviate ¬[α]¬*A* to
<α>*A* (“some execution of α from the present
state leads to a state where *A* is true”) as in modal
logic. Some standard programming constructs are easily introduced by
definitional abbreviation:

- (
**if***A***then**α**else**β) =_{df}((*A*?;α) ∪ (¬*A*?;β)) - α
^{+}=_{df}(α;α*) - (
**while***A***do**α) =_{df}((*A*?;α)*;¬*A*?) - (
**repeat**α**until***A*) =_{df}(α;((¬*A*;α)*;*A*?)) **abort**=_{df}0?**skip**=_{df}1?

Let us adopt the standard rules for omission of parentheses. We
write α^{n} for α;…;α with
*n* appearances of α. More formally:

- α
^{0}=_{df}1? - α
^{n+1}=_{df}α;α^{n}

Formulas can be used to describe the properties that hold after the
execution of a program. For example, the formula
[α∪β]*A* means that whenever program α or
β is executed, a state is reached where *A* holds whereas
the formula <(α;β)*>*A* means that there is a
sequence of alternating executions of α and β such that a
state is reached where *A* holds. Semantically speaking,
formulas are interpreted by sets of states and programs are
interpreted by binary relations over states in a transition
system. More precisely, the semantics of formulas and programs is
given by so-called Kripke structures
*M* = (*W*, *R*,*V*)
where *W* is a nonempty set of worlds or states, *R* is
a mapping from the set Π_{0} of atomic programs into binary
relations on *W* and *V* is a mapping from the set
Φ_{0} of atomic formulas into subsets of
*W*. Informally, the mapping *R* assigns to each atomic
program π ∈ Π_{0} some binary
relation *R*(π) on *W* with intended meaning
*x**R*(π)*y* iff there exists an execution of
π from *x* that leads to *y*, whereas the mapping
*V* assigns to each atomic formula
*p* ∈ Φ_{0} some subset
*V*(*p*) of *W* with intended meaning
*x* ∈ *V*(*p*) iff *p*
is true in *x*. Given our readings of 0, ¬*A*,
*A*∨*B*,
[α]*A*, α;β, α∪β, α* and
*A*?, it is clear that *R* and *V* must be
extended inductively as follows to supply the intended meanings for
the complex programs and formulas:

*x**R*(α;β)*y*iff there exists a world*z*such that*x**R*(α)*z*and*z**R*(β)*y**x**R*(α∪β)*y*iff*x**R*(α)*y*or*x**R*(β)*y**x**R*(α*)*y*iff there exists a non-negative integer*n*and there exist worlds*z*_{0}, …,*z*_{n}such that*z*_{0}=*x*,*z*_{n}=*y*and for all*k*= 1..*n*,*z*_{k−1}*R*(α)*z*_{k}*x**R*(*A*?)*y*iff*x*=*y*and*y*∈*V*(*A*)*V*(0) = ∅*V*(¬*A*) =*W*\*V*(*A*)*V*(*A*∨*B*) =*V*(*A*) ∪*V*(*B*),*V*([α]*A*) = {*x*: for all worlds*y*, if*x**R*(α)*y*then*y*∈*V*(*A*)}

If *x* ∈ *V*(*A*) then we
say that *A* is satisfied at state *x* in *M*, or
“*M*, *x* sat *A*”. Now consider a formula
*A*. We shall say that *A* is valid in *M* or
that *M* is a model of *A*, or “*M*
⊨ *A*”,
iff for all worlds *x*,
*x* ∈ *V*(*A*). *A* is
said to be valid, or
“⊨
*A*”, iff for all models *M*, *M*
⊨
*A*. We shall say that *A* is satisfiable in *M*
or that *M* satisfies *A*, or “*M* sat
*A*”, iff there exists a world *x* such that
*x* ∈ *V*(*A*). *A* is
said to be satisfiable, or “sat *A*”, iff there exists a model
*M* such that *M* sat *A*. Interestingly,

satAiff not ⊨ ¬A

⊨Aiff not sat ¬A

The reader may easily verify that

⊨ [α;β]A↔ [α][β]A

⊨ [α∪β]A↔ [α]A∧ [β]A

⊨ [α*]A↔A∧ [α][α*]A

⊨ [A?]B↔ (A→B)

In other respects,

⊨ [ifAthenαelseβ]B↔ (A∧ [α]B) ∨ (¬A∧ [β]B)

⊨ [α^{+}]A↔ [α](A∧ [α^{+}]A)

⊨ [whileAdoα]B↔ (¬A∧B) ∨ (A∧ [α][whileAdoα]B)

⊨ [repeatαuntilA]B↔ [α]((A∧B) ∨ (¬A∧ [repeatαuntilA]B))

⊨ [abort]0

⊨ [skip]A↔A

It is the valid formulas above that lead to the following
definition. Let *X* be a set of formulas. The Fischer-Ladner
closure of *X* is the least set FL(*X*) of formulas
containing *X* and such that

- FL(
*X*) is closed under subformulas - FL(
*X*) is closed under single negations - If [α;β]
*A*∈ FL(*X*) then [α][β]*A*∈ FL(*X*) - If [α∪β]
*A*∈ FL(*X*) then [α]*A*∈ FL(*X*) and [β]*A*∈ FL(*X*) - If [α*]
*A*∈ FL(*X*) then [α][α*]*A*∈ FL(*X*) - If [
*A*?]*B*∈ FL(*X*) then*A*∈ FL(*X*)

It is important to remark that both the number and the size of the
formulas in FL(*X*) are linearly bounded by the size of
*X*. Note also that

FL(FL(X)) = FL(X)

IfX⊆Ythen FL(X) ⊆ FL(Y)

Hence,

IfX⊆ FL(Y) then FL(X) ⊆ FL(Y)

Let Γ be a set of formulas and *A* be a formula. We
shall say that Γ logically implies *A*, or “Γ
⊨
*A*”, iff *A* is valid in every model of all formulas
in Γ. Γ is said to be logically satisfiable with
*A*, or “Γ sat *A*”, iff *A* is satisfiable
in some model of all formulas in Γ. Therefore,

Γ satAiff not Γ ⊨ ¬A

Γ ⊨Aiff not Γ sat ¬A

Moreover,

satAiff ∅ satA

⊨Aiff ∅ ⊨A

If Γ is finite then let π_{1}, …,
π_{m} be all atomic programs occurring in
Γ∪{*A*} and Γ′ be the conjunction of all
formulas in Γ. Then,

Γ satAiff sat [(π_{1}∪…∪π_{m})*]Γ′ ∧A

Γ ⊨Aiff ⊨ [(π_{1}∪…∪π_{m})*]Γ′ →A

Given two Kripke structures
*M* = (*W*, *R*,*V*)
and *M*′ = (*W*′,
*R*′, *V*′), one may ask whether
they satisfy the same formulas. The notion of bisimulation has become
the standard measure for equivalence of Kripke structures. A
*bisimulation* between the Kripke structures
*M* = (*W*, *R*,*V*)
and *M*′ = (*W*′,
*R*′, *V*′) is a binary relation
*Z* between their states such that for all worlds *x* in
*M* and for all worlds *x*′ in *M*′,
if *xZx*′ then

- for all atomic formulas
*p*∈ Φ_{0},*x*∈*V*(*p*) iff*x*′∈*V*′(*p*) - for all atomic programs π ∈
Π
_{0}and for all worlds*y*in*M*, if*x**R*(π)*y*then there exists a world*y*′ in*M*′ such that*yZy*′ and*x*′*R*′(π)*y*′ - for all atomic programs π ∈
Π
_{0}and for all worlds*y*′ in*M*′, if*x*′*R*′(π)*y*′ then there exists a world*y*in*M*such that*yZy*′ and*x**R*(π)*y*

It is known since the beginning of PDL that for all worlds *x*
in *M* and for all worlds *x*′ in
*M*′, if *xZx*′ then for all formulas
*A*, *x* ∈ *V*(*A*)
iff *x*′
∈ *V*′(*A*). Van Benthem [1998] has
showed that the programming constructs α;β,
α∪β and [α]0? completely characterize the
first-order program operations that are safe for bisimulation.

The following sections provide the proof theory and complexity
theory of PDL. The purpose of the proof theory is to provide the
characterization of the property
⊨
*A* in terms of axioms and rules of inference. The aim of the
complexity theory is to establish the computability of the property
sat *A* in terms of resources of time or space.

## 3. Axiomatization and completeness

The goal is to define a deducibility predicate
⊢ inductively by operations on
formulas that depend only on their syntactic structure in such a way
that for all formulas *A*,

⊢Aiff ⊨A.

Let ⊢ be the deducibility predicate corresponding in the language of propositional dynamic logic to the least normal modal logic containing every instance of the following axiom schemas:

(A1) [α;β]A↔ [α][β]A

(A2) [α∪β]A↔ [α]A∧ [β]A

(A3) [α*]A↔A∧ [α][α*]A

(A4) [A?]B↔ (A→B)

and closed under the following rule of inference:

(I) fromA→ [α]AinferA→ [α*]A

If *X* is a set of formulas and *A* is a formula then we
say that *A* is
⊢-deducible
from *X*, or “*X*
⊢
*A*”, if there exists a sequence *A*_{0},
*A*_{1}, …, *A*_{n} of
formulas such that
*A*_{n} = *A* and for all
*i*≤*n*, *A*_{i} is an
instance of an axiom schema, or a formula of *X*, or comes from
earlier formulas of the sequence by a rule of inference. Further,
⊢
*A* iff ∅
⊢
*A*; in this case we say that *A* is
⊢-deducible.
*X* is said to be
⊢-consistent
iff not *X*
⊢
0. It is easy to establish that (I) can be replaced by the following
axiom schema:

(A5) [α*](A→ [α]A) → (A→ [α*]A)

Let us first establish that (I) is a derived rule of the proof system based on (A1), (A2), (A3), (A4) and (A5):

1. A→ [α]Apremise 2. [α*]( A→ [α]A)from 1 using generalization 3. [α*]( A→ [α]A) → (A→ [α*]A)axiom schema (A5) 4. A→ [α*]Afrom 2 and 3 using modus ponens

Let us next establish that (A5) is ⊢-deducible:

1. [α*]( A→ [α]A) ↔

(A→ [α]A) ∧ [α][α*](A→ [α]A)axiom schema (A3) 2. A∧ [α*](A→ [α]A) →

[α](A∧ [α*](A→ [α]A))from 1 using propositional calculus and distributivity of [α] over ∧ 3. A∧ [α*](A→ [α]A) →

[α*](A∧ [α*](A→ [α]A))from 2 using (I) 4. [α*]( A→ [α]A) → (A→ [α*]A)from 3 using propositional calculus and distributivity of [α*] over ∧

The axiomatization of PDL based on axiom schemes (A1), (A2), (A3), (A4) and (A5) has been proposed in Segerberg [1977]. It is immediate from the definitions above that ⊢ is sound with respect to ⊨, i.e.

For all formulasA, if ⊢Athen ⊨A

The proof proceeds by induction on the length of *A*'s
deduction in
⊢.
The completeness of
⊢
with respect to
⊨,
i.e.

For all formulasA, if ⊨Athen ⊢A

led to problems that occupied several researchers. The line of reasoning presented by Segerberg [1977] was the first attempt to prove the completeness of ⊢, but there was a mistake in Segerberg's argument. Segerberg took five years to obtain a full corrected proof. In the meantime, Parikh [1978a] had published what can be considered the first proof of the completeness of ⊢. Whereas unpublished proofs of completeness were also put into circulation at this time, e.g. Gabbay's proof, very different proofs of completeness have been published since, e.g. Kozen and Parikh [1981]. And, finally, let us mention the completeness of the sequential systems proposed by Nishimura [1979] and Vakarelov [1983] which constitute alternative proof theories of PDL. An alternative formulation of a deducibility predicate for PDL allows the use of an infinitary rule of inference. Let ⊢′ be the deducibility predicate corresponding in the language of propositional dynamic logic to the least normal modal logic containing every instance of the axiom schemas (A1), (A2), (A3) and (A4) and closed under the following infinitary rule of inference:

(I′) from {[β][α^{n}]A:n≥ 0} infer [β][α*]A

It can be proved that ⊢′ is both sound and complete with respect ⊨, i.e.

For all formulasA, ⊢′Aiff ⊨A

In other words, as far as generating the set of all valid formulas is concerned, the proof systems ⊢ and ⊢′ are equivalent.

## 4. Decidability and complexity

In this section, we investigate the complexity of the following decision problem:

(SAT) Given a formulaA, isAsatisfiable?

One of the earliest results on PDL was the proof that PDL has the finite model property, i.e.

For all formulasA, if satAthen there exists a finite modelMsuch thatMsatA

The finite model property was first proved by Fischer and Ladner [1979]. Together with the axiomatization of PDL, the finite model property guarantees decidability of (SAT), since

- It is possible to generate all formulas
*A*such that not sat*A* - For all positive integers
*n*, it is possible to generate all distinct representations of models*M*that have size at most*n* - For all formulas
*A*and for all finite models*M*, it is possible to test if*M*sat*A*

The existence of a NEXPTIME algorithm deciding (SAT) comes from Fischer and Ladner [1979], too, who showed in fact that PDL has the small-model property, i.e.

For all formulasA, if satAthen there exists a finite modelMof size exponential inAsuch thatMsatA

The proof of Fischer and Ladner [1979] relies on the implicit
hypothesis that
⊢
is complete with respect to
⊨.
A proof that does not rely on the assumption that PDL is complete has
been presented by Kozen and Parikh [1981] who considered, given a
formula *A* such that *A* is PDL-consistent, the set
ConAt(*A*) of all those atoms in the Boolean algebra generated
by FL({*A*}) which are PDL-consistent. These are subsets of
the following set of formulas:

FL^{¬}({A}) = FL({A}) ∪ {¬B:B∈ FL({A})}

Kozen and Parikh defined a Kripke structure
*M* = (*W*, *R*,*V*)
based on ConAt(*A*) as follows:

*W*= ConAt(*A*)- For all atomic programs π ∈ Π
_{0}and for all*x*,*y*∈ ConAt(*A*),*x**R*(π)*y*iff*x*∧ <π>*y*is PDL-consistent - For all atomic formulas
*p*∈ Φ_{0}and for all*x*∈ ConAt(*A*),*x*∈*V*(*p*) iff*p*∈*x*

where we write *x* and *y* both for the consistent
atoms and for the conjunctions over their members. Note that
*M* is of size at most exponential in *A*. In order to
prove that *M* sat *A*, Kozen and Parikh proved that

- For all programs α and for all
*x*,*y*∈ ConAt(*A*), if*x**R*(α)*y*then*x*∧ <α>*y*is PDL-consistent - For all formulas
*B*∈ FL({*A*}) and for all*x*∈ ConAt(*A*),*M*,*x*⊨*B*iff*B*∈*x*

Since *A* is PDL-consistent, then there exists
*x* ∈ ConAt(*A*) such that
*A* ∈ *x*. Consequently, *M*,
*x* sat *A*. Therefore *M* sat *A*. The
key results in the complexity theory of PDL come from Fischer and
Ladner [1979] and Prat [1980]. Observing that a formula of PDL can
efficiently describe the computation of a linear-space–bounded
alternating Turing machine, Fischer and Ladner [1979] first
established the lower bound of exponential time of (SAT). The EXPTIME
upper bound of (SAT) has been obtained by Pratt [1980], who used the
equivalent for PDL of the method of tableaux.

## 5. Variants

Results concerning comparative power of expression, decidability, complexity, axiomatization and completeness of a number of variants of PDL obtained by extending or restricting its syntax and its semantics constitute the subject of a wealth of literature.

### 5.1 PDL without tests

The axiom schema [*A*?]*B* ↔ (*A* →
*B*) seems to indicate that for every formula *C*, there
exists an equivalent test-free formula*C*′—i.e.,
there is a test-free formula *C*′ such that
⊨ *C* ↔
*C*′. It is interesting to observe that this assertion
is untrue. Let PDL_{0} be the restriction of PDL to test-free
regular programs, i.e. programs which do not contain tests. Berman and
Paterson [1981] considered the PDL formula

<until¬pdoπ><π>p

and proved that there is no PDL_{0} formula equivalent to
it. Hence, PDL has more expressive power than PDL_{0}. Their
argument actually can be generalized as follows. For all
*n* ≥ 0, let PDL_{n+1} be the
subset of PDL in which programs can contain tests *A*? only if
*A* is a PDL_{n} formula. For all
*n* ≥ 0, Berman and Paterson considered the
PDL_{n+1} formula *A*_{n+1}
defined by

<until¬A_{n}doπ_{n}>< π_{n}>A_{n}

where *A*_{0} = *p* and
π_{0} = π and proved that for all
*n* ≥ 0, there is no PDL_{n}
formula equivalent to *A*_{n+1}. Hence, for
all *n* ≥ 0, PDL_{n+1} has
more expressive power than PDL_{n}.

### 5.2 PDL with converse

CPDL is the extension of PDL with converse. For all programs
α, let α^{-1} stand for a new program with
semantics

xR(α^{-1})yiffyR(α)x.

The converse construct allows us to express facts about states preceding the current one and to reason backward about programs. As a result, we have

⊨A→ [α]<α^{-1}>A,

⊨A→ [α^{-1}]<α>A.

The addition of the converse construct does not change the properties of PDL in any significant way. In fact, by adding every instance of the following axiom schemas:

(A6)A→ [α]<α^{-1}>A

(A7)A→ [α^{-1}]<α>A

to the proof system of section 3, we obtain a sound and complete deducibility predicate in the extended language. See Parikh [1978a] for details. Of course, the lower bound of exponential time of (PDL-SAT) also yields the same lower bound of (CPDL-SAT). Since, moreover, CPDL satisfies, according to Vakarelov [1983], the same small-model property as PDL:

For all CPDL formulasA, if satAthen there exists a finite modelMof size exponential inAsuch thatMsatA

satisfiability in CPDL is decidable in nondeterministic exponential
time. Although many authors have asserted that the proof that
(PDL-SAT) is in EXPTIME extends to the proof that (CPDL-SAT) is in
EXPTIME too without difficulties, the first efficient EXPTIME
algorithm for CPDL is presented in De Giacomo and Massacci [2000]. De
Giacomo [1996] presents a mapping *t* from CPDL formulas into
PDL formulas such that

- For all CPDL formulas
*A*,*A*is satisfiable iff*t*(*A*) is satisfiable - The size of
*t*(*A*) is polynomial in the size of*A* *t*(*A*) is easily obtained from*A*by operations that depend only on*A*'s syntactic structure

Nevertheless, it is interesting to remark that CPDL has more
expressive power than PDL. To see this, consider the CPDL formula
<π^{-1}>1 and the Kripke structures
*M* = (*W*, *R*,*V*)
and
*M*′ = (*W*′, *R*′,*V*′)
where *W* = {*x*,*y*},
*R*(π) = {(*x*, *y*)},
*W*′ = {*y*′},
*R*′(π) = ∅
and *y* and *y*′ satisfy the
same atomic formulas. Since *M*, *y* sat
<π^{-1}>1, not *M*′, *y*′
sat <π^{-1}>1 and for all PDL formulas *A*,
*M*, *y* sat *A* iff *M*′,
*y*′ sat *A*, it is clear that no PDL formula is
equivalent to <π^{-1}>1.

### 5.3 PDL with infinite and cyclic repeating

Propositional dynamic logic with repeating, RPDL, was introduced by Streett [1982]. It contains, for all programs α, the expression α! standing for a new formula with semantics

V(α!) = {x: there exists an infinite sequencex_{0},x_{1}, … of states such thatx_{0}=xand for alln≥ 0,x_{n}R(α)x_{n+1}}

Then, α! is taken to be satisfied in *x* if α
can be repeatedly executed infinitely many times. As a result, we
have

⊨ α! → <α>α!,

⊨ [α*](A→ <α>A) → (A→ α!)

Streett [1982] proposed an axiomatization of RPDL by adding to the proof system of section 3 every instance of the following schemas:

(A8) α! → <α>α!

(A9) [α*](A→ <α>A) → (A→ α!)

Note that the formula

<α>α! → α!

is deducible in any proof system containing (A8) and (A9):

1. α! → <α>α! axiom schema (A8) 2. <α>α! → <α><α>α! from 1 using propositional calculus, distributivity of [α] over ∧ and generalization 3. [α*](<α>α! → <α><α>α!) from (2) using generalization 4. [α*](<α>α! → <α><α>α!) → (<α>α! → α!) axiom schema (A9) 5. <α>α! → α! from (3) and (4) using modus ponens

Completeness of this proof system is treated in Sakalauskaite and Valiev [1990]. Concerning the complexity theory of RPDL, Streett [1982] demonstrated that

For all RPDL formulasA, if satAthen there exists a finite modelMsuch thatMsatA

whereas it is still unknown whether

For all RPDL formulasA, if satAthen there exists a finite modelMof size exponential inAsuch thatMsatA

It is here that the decidability of (RPDL-SAT) in deterministic triple exponential time is established. The gap between this upper bound for deciding (RPDL-SAT) and the simple exponential-time lower bound for deciding (PDL-SAT) remains open.

Finally it can be shown that RPDL has more expressive power than
PDL. Consider the RPDL formula π! and suppose that there exists a
PDL formula *A* such that
⊨
π! ↔ *A*. Without loss of generality, we may assume
that *A* contains no atomic formula. We may also assume that
π is the only atomic program occurring in *A*. Let
*M* be the Kripke structure
(*W*, *R*,*V*) where

W= {0,1,…}

xR(π)yiffy=x-1

For all *x* ∈ *W*, we have

notM,xsat π!

Hence for all *x* ∈ *W*

notM,xsatA

Let
*M*′ = (*W*′, *R*′,*V*′)
be the Kripke structure obtained from *M* by identifying states
indistinguishable by the subformulas of *A*. Since PDL
possesses the collapsed-model property, for all
*x*′ ∈ *W*′, not
*M*′, *x*′
⊨
*A*. Consequently, for all
*x*′ ∈ *W*′, not
*M*′, *x*′
⊨
π!. Since *M*′ is obtained from *M* by
identifying some pair of distinct states, it turns out that there
exists *x*′ ∈ *W*′ such
that *M*′, *x*′
⊨
π!: a contradiction.

There are other ways of making possible the assertion that a
program can execute forever: add, for all programs α, the
formulas **loop**(α) and
**cycle**(α) with semantics

V(loop(α)) = {x:xR(α)x}

V(cycle(α)) = {x:xR(α^{+})x}

Hence, **loop**(α) is satisfied at some state
*x* if there exists an α-cycle of length 1 containing
*x*, whereas **cycle**(α) is satisfied at
some state *x* if there exists an α-cycle containing
*x*. Note that **cycle** is definable in PDL with
**loop**:

⊨cycle(α) ↔loop(α^{+})

This motivates the following questions:

Isloopdefinable in PDL withcycle?

Isrepeatdefinable in PDL withloop?

Isloopdefinable in RPDL?

Isrepeatdefinable in PDL withcycle?

Iscycledefinable in RPDL?

Here, we sketch the proof that **loop** is not
definable in PDL with **cycle**. The proofs that
**repeat** is not definable in PDL with
**loop**, **loop** is not definable in RPDL,
**repeat** is not definable in PDL with
**cycle** and **cycle** is not definable in
RPDL are similar. Consider the formula **loop**(π) and
suppose that there exists a formula *A* in PDL with
**cycle** such that
⊨
**loop**(π) ↔ *A*. Without loss of
generality, we may assume that *A* contains no atomic
formula. We may also assume that π is the only atomic program
occurring in *A*. Now consider the Kripke structures
*M* = (*W*, *R*,*V*)
and
*M*′ = (*W*′, *R*′,*V*′)
where *W* = {*x*,*y*},
*R*(π) = {(*x*,*y*),(*y*,*x*)},
*W*′ = {*y*′},
*R*′(π) = {(*y*′,*y*′)}
and *x*, *y* and *y*′ satisfy the same
atomic formulas. Since not *M*, *x* sat
**loop**(π), not *M*, *y* sat
**loop**(π), *M*′, *y*′ sat
**loop**(π) and for all formulas *A* in PDL
with **cycle**, *M*, *x* sat *A* iff
*M*, *y* sat *A* iff *M*′,
*y*′ sat *A*, it is clear that no formula in PDL
with **cycle** is equivalent to
**loop**(π). Let us also remark that neither PDL with
**loop** nor PDL with **cycle** possesses
the finite-model property. For example, the formula

[π*](<π>1 ∧ ¬cycle(π))

is satisfiable in infinite Kripke structures only. Through a
reduction to the emptiness problem for some restricted version of tree
automata, Danecki [1984a] established the decidability of (SAT) for
PDL formulas with **loop** in deterministic exponential
time. It must be finally said that no complete finitary axiomatization
of PDL with **loop** or PDL with **cycle**
is known.

### 5.4 PDL with intersection

Another construct has been studied: the intersection of programs. By adding intersection of programs to PDL, we obtain the logic IPDL. In IPDL, for all programs α, β, the expression α∩β stands for a new program with semantics

xR(α∩β)yiffxR(α)yandxR(β)y

For instance, the intended reading of
<α∩β>*A* is that if we execute α and
β in the present state then there exists a state reachable by
both programs which satisfies *A*. As a result, we have

⊨ <α∩β>A→ <α>A∧ <β>A

but, in general, we have

not ⊨ <α>A∧ <β>A→ <α∩β>A

Note also that we have

⊨ [(α;(A∧ [(β;B?;α)∩A?]0)?;β) ∩B?]0

Let us note that the constructs **loop**(α) and
**cycle**(α) can be expressed in IPDL. In
propositional dynamic logic with intersection, they are respectively
equivalent to <α∩1?>1 and
<α^{+}∩1?>1. Although intersection of programs
plays an important role in various applications of PDL to artificial
intelligence and computer science, the proof theory and the complexity
theory of PDL with intersection remained unexplored for several
years. Concerning the complexity theory of IPDL, difficulties appear
when one considers the finite model property. In fact, the formula

[π*](<π>1 ∧ [π*∩1?]0)

is satisfiable in infinite Kripke structures only. In other words,
IPDL does not possess the finite-model property. Danecki [1984b]
investigated the complexity theory of IPDL and showed that deciding
(IPDL-SAT) can be done in deterministic double exponential time. The
complexity gap between this double exponential-time upper bound for
deciding (IPDL-SAT) and the simple exponential-time lower bound for
deciding (PDL-SAT) obtained by Fischer and Ladner [1979] remained open
for more than twenty years. In 2004, Lange [2005] established the
lower bound of exponential space of (IPDL-SAT). In 2006, Lange and
Lutz [2005] gave a proof of a double exponential-time lower bound of
the satisfiability problem for IPDL without tests by a reduction from
the word problem of exponentially space-bounded alternating Turing
machines. In this reduction, the role of the iteration construct is
essential since, according to Massacci [2001], the satisfiability
problem for iteration-free IPDL without tests is only
PSPACE-complete. Adding the converse construct to IPDL, we obtain
ICPDL. The satisfiability problem of ICPDL has been recently proved to
be decidable in double exponential-time by Göller, Lohrey and
Lutz [2007]. Let us remark that, in ICPDL,
**cycle**(α) is equivalent to
<α*∩α^{-1}>1. Concerning the proof
theory of IPDL, difficulties appear when we realize that no axiom
schema, in the language of PDL with intersection, corresponds to the
semantics

xR(α∩β)yiffxR(α)yandxR(β)y

of the expression α∩β in the sense, for example,
that the axiom schemas (A1) and (A2) respectively correspond to the
semantics of the expressions α;β and α∪β.
For this reason, the axiomatization of PDL with intersection was open
until the complete proof system developed in Balbiani and Vakarelov
[2003]. In another variant of PDL, due to Peleg [1987] and
studied by Goldblatt [1992], the expression α∩β is
interpreted “do α and β in parallel”. In this context, the
binary relations *R*(α) and *R*(β) are no
longer sets of pairs of the form (*x*,*y*) with
*x*, *y* worlds, but rather sets of pairs of the form
(*x*,*Y*) with *x* a world and *Y* a set
of worlds.

### 5.5 Restriction to structured programs

Let SPDL be the restriction of PDL in which the program constructs
∪ and * are allowed to appear only in the conditional and
**while** loop constructs (**if** *A*
**then** α **else** β) and
(**while** *A* **do** α) found
in conventional programming languages. Hence SPDL is the variant of
PDL defined as follows:

- Every atomic formula is a formula
- 0 is a formula
- If
*A*is a formula then ¬*A*is a formula - If
*A*and*B*are formulas then (*A*∨*B*) is a formula - If α is a program and
*A*is a formula then [α]*A*is a formula - Every atomic program is a program
- If α and β are programs then (α;β) is a program
- If
*A*is a formula and α and β are programs then (**if***A***then**α**else**β) is a program - If
*A*is a formula and α is a program then (**while***A***do**α) is a program - If
*A*is a formula then*A*? is a program

This restriction to structured programs leads to a loss of expressive power. Halpern and Reif [1983], for example, proved that the PDL formula

<(π∪π′)*>p

has no equivalent in SPDL. It is thus natural to ask whether this restriction to structured programs gives us an easier solution to the satisfiability decision problem. According to Harel [1984], it turns out that SPDL is very similar to PDL with respect to decidability, since the deterministic exponential-time lower bound of (PDL-SAT) carries over to (SPDL-SAT).

### 5.6 Deterministic programs

One natural variant of PDL is semantical rather than syntactical.
It consists in requiring atomic programs to be deterministic so that,
in terms of the binary relation *R*(π) assigned to each
atomic program π ∈ Π_{0}, we have for
all states *x*, *y*, *z*,

IfxR(π)yandxR(π)ztheny=z

—i.e. *R*(π) becomes a partial function on the set
of all states. Obviously, formulas valid in the class of all models
are also valid in the restricted class of all deterministic models,
i.e. models in which *R*(π) is a partial function for each
π ∈ Π_{0}. In other respects, the
instances of the schema

<π>A→ [π]A

are valid in each deterministic model. As well, the instances of the schema

[π](A∨B) → [π]A∨ [π]B

are also valid in each deterministic model. Consequently, no instance of the schemas

<π>A∧ <π>¬A

[π](A∨B) ∧ <π>¬A∧ <π>¬B

is satisfiable in the class of all deterministic models. Let DPDL be the logic with the same syntax as PDL but with its semantics restricted to deterministic models. It becomes natural to ask whether this restriction to deterministic models gives rise to a set of valid formulas that can be axiomatized and to a set of satisfiable formulas that can be decided. That satisfiability of formulas in the class of all deterministic models is decidable is proved in Parikh [1978b]. However, Parikh's decision procedure has no elementary bounds. Later, Valiev [1980] established that (DPDL-SAT) is EXPTIME-hard whereas Ben-Ari, Halpern and Pnueli [1982] presented a decision procedure for the satisfiability of formulas in deterministic models that runs in deterministic exponential time. Ben-Ari, Halpern and Pnueli also demonstrated that the proof system obtained by adding every instance of the axiom schema

(A10) <π>A→ [π]A

to the proof system of section 3 is sound and complete. Three years
earlier, Valiev [1979] presented a complete sequential system in the
spirit of the Gentzen type axiomatization of PDL elaborated by Pratt
[1978]. Thus, apparently, requiring atomic programs to be
deterministic presents no problem. It is a mere façade. In
fact, for many syntactical variants of PDL, their deterministic
versions make up logics whose set of satisfiable formulas is not
decidable or whose set of valid formulas is not
axiomatizable. According to Harel [1983], formulas of IPDL, for
example, interpreted over deterministic Kripke structures give rise to
a highly undecidable satisfiability problem. According to Danecki
[1984b], a similar phenomenon occurs with formulas of PDL with
**loop**. Nevertheless, it is still unknown whether the
restriction of formulas of IPDL to structured programs gives rise,
interpreted over deterministic structures, to a decidable
satisfiability problem.

## 6. Conclusion

This article has focused on propositional dynamic logic and some of its syntactical or semantical variants:

- PDL without tests
- PDL with converse
- PDL with intersection
- PDL with infinite and cyclic repeating
- restriction to structured programs
- deterministic programs

PDL was conceived primarily for reasoning about programs. There are by now a number of other applications of modal logic to reasoning about programs:

- temporal logic
- μ-calculus
- algorithmic logic
- process logic
- real-time logic

In other applications, PDL can also be used for reasoning about actions.

## Bibliography

- Balbiani, P., and D. Vakarelov, 2003, “PDL with intersection of
programs: a complete axiomatization”,
*Journal of Applied Non-Classical Logics*, 13: 231-276. - Ben-Ari, M., Halpern, J., and A. Pnueli, 1982, “Deterministic
propositional dynamic logic: finite models, complexity, and
completeness”,
*Journal of Computer and System Sciences*, 25: 402-417. - van Benthem, J., 1998, “Program constructions that are safe
for bisimulation”,
*Studia Logica*, 60: 311-330. - Berman, F., and M. Paterson, 1981, “Propositional dynamic logic is
weaker without tests”,
*Theoretical Computer Science*, 16: 321-328. - Danecki, R., 1984a, “Propositional dynamic logic with strong loop
predicate”, In M. Chytil and V. Koubek,
*Mathematical Foundations of Computer Science*, Berlin: Springer-Verlag, 1984, 573-581. - –––, 1984b, “Nondeterministic propositional
dynamic logic with intersection is decidable”, In A. Skowron (ed.),
*Computation Theory*, Berlin: Springer-Verlag, 34-53. - De Giacomo, G., 1996, “Eliminating ‘converse’ from
converse PDL”,
*Journal of Logic, Language and Information*, 5: 193-208. - De Giacomo, G., and F. Massacci, 2000, “Combining deduction and
model checking into tableaux and algorithms for converse-PDL”,
*Information and Computation*, 160: 109-169. - Engeler, E., 1967, “Algorithmic properties of structures”,
*Mathematical Systems Theory*, 1: 183-195. - Fischer, M., and R. Ladner, 1979, “Propositional dynamic logic of
regular programs”,
*Journal of Computer and System Sciences*, 18: 194-211. - Goldblatt, R., 1982,
*Axiomatising the Logic of Computer Programming*, Berlin: Springer-Verlag. - –––, 1992,
*Logics of Time and Computation*, Stanford: Center for the Study of Language and Information Publications. - Göller, S., Lohrey, M., and C. Lutz, 2007, “PDL with intersection and converse is 2EXP-complete”, forthcoming.
- Halpern, J., and J. Reif, 1983, “The propositional dynamic logic
of deterministic, well-structured programs”,
*Theoretical Computer Science*, 27: 127-165. - Harel, D., 1979,
*First-Order Dynamic Logic*, Berlin: Springer-Verlag. - –––, 1983, “Recurring dominoes: making the
highly undecidable highly understandable”, In M. Karpinski (ed.),
*Foundations of Computation Theory*, Berlin: Springer-Verlag, 177-194. - –––, 1984, “Dynamic logic”, In D. Gabbay and
F. Guenthner (eds.),
*Handbook of Philosophical Logic*, Volume II, Dordrecht: D. Reidel, 497-604. - Harel, D., Kozen, D., and J. Tiuryn, 2000,
*Dynamic Logic*, Cambridge, MA: MIT Press. - Hoare, C., 1969, “An axiomatic basis for computer
programming”,
*Communications of the ACM*, 12: 576-580. - Kozen, D., and R. Parikh, 1981, “An elementary proof of the
completeness of PDL”,
*Theoretical Computer Science*, 14: 113-118. - Kozen, D., and J. Tiuryn, 1990, “Logics of programs”, In J. Van
Leeuwen (ed.),
*Handbook of Theoretical Computer Science*, Volume B, Amsterdam: Elsevier, 789-840. - Lange, M., 2005, “A lower complexity bound for propositional
dynamic logic with intersection”, In R. Schmidt, I. Pratt-Hartmann,
M. Reynolds and H. Wansing (eds.),
*Advances in Modal Logic*, Volume 5, London: King's College Publications, 133-147. - Lange, M., and C. Lutz, 2005, “2-EXPTIME lower bounds for
propositional dynamic logics with intersection”,
*Journal of Symbolic Logic*, 70: 1072-1086. - Lutz, C., 2005, “PDL with intersection and converse is
decidable”. In L. Ong (ed.),
*Computer Science Logic*, Berlin: Springer-Verlag, 413-427. - Massacci, F., 2001, “Decision procedures for expressive
description logics with intersection, composition, converse of roles
and role identity”, In B. Nebel (ed.),
*17th International Joint Conference on Artificial Intelligence*, San Francisco: Morgan Kaufmann, 193-198. - Mirkowska, G., and A. Salwicki, 1987,
*Algorithmic Logic*, Dordrecht: D. Reidel. - Nishimura, H., 1979, “Sequential method in propositional dynamic
logic”,
*Acta Informatica*, 12: 377-400. - Parikh, R., 1978a, “The completeness of propositional dynamic
logic”, In J. Winkowski (ed.),
*Mathematical Foundations of Computer Science*, Berlin: Springer-Verlag, 1978, 403-415. - –––, 1978b, “A decidability result for a second
order process logic”, In
*19th Annual Symposium on Foundations of Computer Science*. New York: IEEE, 1978, 177-183. - –––, 1983, “Propositional logics of programs: new
directions”, In M. Karpinski (ed.),
*Foundations of Computation Theory*, Berlin: Springer-Verlag, 347-359. - Peleg, D., 1987, “Concurrent dynamic logic”,
*Journal of the ACM*, 34: 450-479. - Pratt, V., 1976, “Semantical considerations on Floyd-Hoare logic”,
In
*Proceedings of the 17th IEEE Symposium on Foundations of Computer Science*, 109-121. - –––, 1978, “A practical decision method for
propositional dynamic logic”, In
*Proceedings of the 10th Annual ACM Symposium on Theory of Computing*, 326-337. - –––, 1980, “A near-optimal method for reasoning
about action”,
*Journal of Computer and System Sciences*, 20: 231-254. - Sakalauskaite, J., and M. Valiev, 1990, “Completeness of
propositional dynamic logic with infinite repeating”, In P. Petkov
(ed.),
*Mathematical Logic*, New York: Plenum Press, 339-349. - Salwicki, A., 1970, “Formalized algorithmic languages”,
*Bulletin de l'Academie Polonaise des Sciences, Serie des sciences mathematiques, astronomiques et physiques*, 18: 227-232. - Segerberg, K., 1977, “A completeness theorem in the modal logic of
programs”,
*Notices of the American Mathematical Society*, 24: 522. - Streett, R., 1982, “Propositional dynamic logic of looping and
converse is elementary decidable”,
*Information and Control*, 54: 121-141. - Vakarelov, D., 1983, “Filtration theorem for dynamic algebras with
tests and inverse operator”, In A. Salwicki (ed.),
*Logics of Programs and their Applications*, Berlin: Springer-Verlag, 314-324. - Valiev, M., 1979, “On axiomatization of deterministic
propositional dynamic logic”, In J. Becvar (ed.),
*Mathematical Foundations of Computer Science*, Berlin: Springer-Verlag. - –––, 1980, “Decision complexity of variants of
propositional dynamic logic”, In P. Dembinski (ed.),
*Mathematical Foundations of Computer Science*, Berlin: Springer-Verlag, 656-664. - Yanov, J., 1959, “On equivalence of operator schemes”,
*Problems of Cybernetic*, 1: 1-100.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

[Please contact the author with suggestions.]

## Related Entries

logic: action | logic: epistemic | logic: modal | logic: temporal