Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

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:

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:

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

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 xR(π)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:

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,

sat A iff not ⊨ ¬A
⊨ A iff not sat ¬A

The reader may easily verify that

⊨ [α;β]A ↔ [α][β]A
⊨ [α∪β]A ↔ [α]A ∧ [β]A
⊨ [α*]A ↔ A ∧ [α][α*]A
⊨ [A?]B ↔ (A → B)

In other respects,

⊨ [if A then α else β]B ↔ (A ∧ [α]B) ∨ (¬A ∧ [β]B)
⊨ [α+]A ↔ [α](A ∧ [α+]A)
⊨ [while A do α]B ↔ (¬A ∧ B) ∨ (A ∧ [α][while A do α]B)
⊨ [repeat α until A]B ↔ [α]((A ∧ B) ∨ (¬A ∧ [repeat α until A]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

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)
If X ⊆ Y then FL(X) ⊆ FL(Y)

Hence,

If X ⊆ 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,

Γ sat A iff not Γ ⊨ ¬A
Γ ⊨ A iff not Γ sat ¬A

Moreover,

sat A iff ∅ sat A
⊨ A iff ∅ ⊨ A

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

Γ sat A iff sat [(π1∪…∪πm)*]Γ′ ∧ A
Γ ⊨ A iff ⊨ [(π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

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,

⊢ A iff ⊨ 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) from A → [α]A infer A → [α*]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 A0, A1, …, An of formulas such that An = A and for all i≤n, Ai 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 → [α]A premise
2.   [α*](A → [α]A) from 1 using generalization
3.   [α*](A → [α]A) → (A → [α*]A) axiom schema (A5)
4.   A → [α*]A from 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 formulas A, if ⊢ A then ⊨ A

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

For all formulas A, if ⊨ A then ⊢ 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 formulas A, ⊢′ A iff ⊨ 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 formula A, is A satisfiable?

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

For all formulas A, if sat A then there exists a finite model M such that M sat A

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

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 formulas A, if sat A then there exists a finite model M of size exponential in A such that M sat A

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:

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

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 formulaC′—i.e., there is a test-free formula C′ such that ⊨ C ↔ C′. It is interesting to observe that this assertion is untrue. Let PDL0 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 ¬p do π><π>p

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

<until ¬An do πn>< πn>An

where A0 = p and π0 = π and proved that for all n ≥ 0, there is no PDLn formula equivalent to An+1. Hence, for all n ≥ 0, PDLn+1 has more expressive power than PDLn.

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)y iff yR(α)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 formulas A, if sat A then there exists a finite model M of size exponential in A such that M sat A

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

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 sequence x0, x1, … of states such that x0 = x and for all n ≥ 0, xnR(α)xn+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 formulas A, if sat A then there exists a finite model M such that M sat A

whereas it is still unknown whether

For all RPDL formulas A, if sat A then there exists a finite model M of size exponential in A such that M sat A

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(π)y iff y = x-1

For all x ∈ W, we have

not M, x sat π!

Hence for all x ∈ W

not M, x sat A

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:

Is loop definable in PDL with cycle?
Is repeat definable in PDL with loop?
Is loop definable in RPDL?
Is repeat definable in PDL with cycle?
Is cycle definable 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(α∩β)y iff xR(α)y and xR(β)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(α∩β)y iff xR(α)y and xR(β)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:

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,

If xR(π)y and xR(π)z then y = 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 was conceived primarily for reasoning about programs. There are by now a number of other applications of modal logic to reasoning about programs:

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

Bibliography

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

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