Logics of programs are modal logics arising from the idea ofassociating a modality \([\alpha]\) with each computer program\(\alpha\) of a programming language. The formula \([\alpha]A\) isthen to be read as: \(A\) is true after the execution of the program\(\alpha\). This idea comes from the line of works by Engeler [1967],Hoare [1969], Yanov [1959], and others who formulated and studiedlogical languages in which the properties of program connectives canbe expressed. The algorithmic logic (AL) first developed by Salwicki[1970] and the dynamic logic (DL) elaborated by Pratt [1976] areproper continuations of these works. We will here concentrate on DL.The numerous papers devoted to DL and its variants as well as its manyapplications in program verification and data structures show that itconstitutes a useful tool for studying the properties of programs.Pratt chose to depict DL on what one might call the first-order level,and it was his work that triggered Fischer and Ladner [1979] to definethe propositional variant of DL a couple of years later. This articlepresents an introduction to PDL, the propositional variant of DL.

• 1. Introduction
• 2. Definitions and fundamental results
  • 2.1 Syntax and semantics
  • 2.2 Axiomatization and completeness
  • 2.3 Decidability and complexity
• 3. Structured programming and correctness of programs
  • 3.1 Hoare calculus
  • 3.2 Hoare calculus and PDL
  • 3.3 Total correctness
• 4. Some variants
  • 4.1 PDL without tests
  • 4.2 PDL with converse
  • 4.3 PDL with repeating and looping
  • 4.4 PDL with intersection
• 5. Conclusion
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Introduction

Dynamic Logics (DL) are modal logics for representing the states andthe events of dynamic systems. The language of DLs is both anassertion language able to express properties of computation states,and a programming language able to express properties of systemtransitions between these states. DLs arelogics of programs,and permit to talk and reason about states of affairs, processes,changes, and results.

Pratt’s original dynamic logic of programs was afirst-order modal logic.Propositional Dynamic Logic(PDL) is the propositional counterpart of it. It was presented as alogic in its own right in Fischer and Ladner [1979]. Beingpropositional, the language of PDL makes no use of terms, predicates,or functions. Thus in PDL, there are two syntactic categories:propositions and programs.

To give meaning to statements in PDL, we typically work with anabstract semantics in terms of Labeled Transition Systems (LTS). LTSscan be seen as a generalization of Kripke models, where transitionsbetween worlds, or states, are “labeled” by names ofatomic programs. A valuation indicates for every state whatpropositions are true in it. A transition labeled \(\pi\)from one state \(x\) to a state \(y\)—noted \(xR(\pi)y\), or\((x,y) \in R(\pi)\)—indicates that starting in \(x\), there isa possible execution of the program \(\pi\) that finishes in \(y\). Ifthe proposition \(A\) is true in \(y\), then the formula\(\langle\pi\rangle A\) is true in \(x\): i.e., in the state \(x\)there is a possible execution of the program \(\pi\) that ends in astate satisfying \(A\). One recognizes in \(\langle\pi\rangle\) amodality reminiscent of the modality of possibility (often noted\(\Diamond\)) of modal logic. Unsurprisingly, there is also acorresponding notion of necessity (whose modality is often noted\(\Box\)). The formula \([\pi]A\) is true in the state \(x\) if \(A\)is true in every state reachable from \(x\) by a transition labeled\(\pi\).

The possible executions of complex programs can be next definedcompositionally. For instance, a program “first \(\alpha\), then\(\beta\)” is a complex program, more specifically asequence. A possible execution can be represented in an LTSby composing a two-step transition—a transition which can besignified by \(R(\alpha;\beta)\)—between the states \(x\) and\(y\): there is a possible execution in the state \(x\) of the program\(\alpha\) that finishes in a state \(z\) and there is a possibleexecution in \(z\) of the program \(\beta\) that finishes in the state\(y\). If the proposition \(A\) is true in \(y\), then the formula\(\langle \alpha;\beta\rangle A\) is be true in the state \(x\). Theprograms \(\alpha\) and \(\beta\) could be complex program themselves.Still more programs can be expressed with more constructs that we willpresent in due time.

A program is then seen in an extensional way: it is a binary relationbetween pairs of states of an LTS. Precisely, it is the set of pairsof the form \((x,y)\) such that the program can be executed in thestate \(x\) and can lead to the state \(y\). On the other hand, aproposition is a statement about a state; it is either true or falsein a state. A proposition can thus also be seen in an extensional way:the set of states of the LTS where it is true.

With the acronym PDL, we refer here precisely to the propositionaldynamic logic with the following program constructs: sequence,non-deterministic choice, unbounded iteration, and test. We present itinsection 2, together with some properties and fundamental results. In particular,we will address its axiomatization and its decidability.

The Hoare calculus from Hoare [1969] is a landmark for logics ofprograms. It concerns the truth of statements of the form\(\{A\}\alpha\{B\}\)—meaning that with the precondition \(A\)the program \(\alpha\) always has \(B\) as a post-condition—andis defined axiomatically. It comes from a want of rigorous methods toreason about the properties of programs, and thus giving to theactivity of programming a certain place in the realm of science.Burstall [1974] saw the analogy between modal logics and reasoningabout programs. But the actual work on it started with Pratt [1976]after it was suggested to him by some of the students of a course hewas giving, specifically about logics of programs. PDL comes fromPratt’s interpretation of Hoare’s calculus in theformalism of modal logic. An introduction to the genesis of PDL can befound in Pratt [1980b]. The Hoare-triple \(\{A\}\alpha\{B\}\) iscaptured by the PDL formula \(A \to [\alpha]B\) meaning literally thatif \(A\) is true, then every successfully terminating execution of\(\alpha\) will end with \(B\) being true. With this connectionrealized, it is a routine to prove the initial rules of Hoare’scalculus using exclusively the axiomatization of PDL. This issomething we will do in detail insection 3 which concentrates on the reasoning about the correctness ofstructured programs.

Additional topics related to PDL include results concerningcomparative power of expression, decidability, complexity, andcompleteness of a number of interesting variants obtained by extendingor restricting PDL in various ways. Since its inception, many variantsof PDL have received attention. These variants may considerdeterministic programs, restricted tests, non-regular programs,programs as automata, complementation and intersection of programs,converse and infinite computations, etc. We will present some of theminsection 4, providing some pointers regarding their relative expressivity, theiraxiomatizations, and their computational complexity.

We conclude insection 5.

2. Definitions and fundamental results

We present the syntax and semantics of PDL insection 2.1. The proof theory of PDL is presented insection 2.2 with axiomatizations and pointers to the literature on completeness.We address the problem of decidability and complexity insection 2.3.

2.1 Syntax and semantics

Propositional dynamic logic (PDL) is designed for representing andreasoning about propositional properties of programs. Its syntax isbased upon two sets of symbols: a countable set \(\Phi_0\) of atomicformulas and a countable set \(\Pi_0\) of atomic programs. Complexformulas and complex programs over this base are defined asfollows.

• Every atomic formula is a formula.
• \(0\) (“false”) is a formula.
• If \(A\) is a formula then \(\lnot A\) (“not \(A\)”)is a formula.
• If \(A\) and \(B\) are formulas then \((A\lor B)\) (“\(A\)or \(B\)”) is a formula.
• If \(\alpha\) is a program andA is a formula then\([\alpha]A\) (“every execution of \(\alpha\) from the presentstate leads to a state where \(A\) is true”) is a formula.
• Every atomic program is a program.
• If \(\alpha\) and \(\beta\) are programs then \((\alpha;\beta)\)(“do \(\alpha\) followed by \(\beta\)”) is a program.
• If \(\alpha\) and \(\beta\) are programs then\((\alpha\cup\beta)\) (“do \(\alpha\) or \(\beta\),non-deterministically”) is a program.
• If \(\alpha\) is a program then \(\alpha^*\) (“repeat\(\alpha\) a finite, but non-deterministically determined, number oftimes”) is a program.
• If \(A\) is a formula then \(A?\) (“proceed if \(A\) istrue, else fail”) is a program.

The other Boolean connectives \(1\), \(\land\), \(\to\), and\(\leftrightarrow\) are used as abbreviations in the standard way. Inaddition, we abbreviate \(\lnot[\alpha]\lnot A\) to\(\langle\alpha\rangle A\) (“some execution of \(\alpha\) fromthe present state leads to a state where \(A\) is true”) as inmodal logic. We write \(\alpha^n\) for \(\alpha;\ldots ;\alpha\) with\(n\) occurrences of \(\alpha\). More formally:

• \(\alpha^0 := 1?\)
• \(\alpha^{n+1} := \alpha;\alpha^n\)

• \(\alpha^+ := \alpha;\alpha^*\)

is often useful to represent an iteration that is unbounded but occursat least once. Finally, we adopt the standard rules for omission ofparentheses.

Formulas can be used to describe the properties that hold after thesuccessful execution of a program. For example, the formula\([\alpha\cup\beta]A\) means that whenever program \(\alpha\) or\(\beta\) is successfully executed, a state is reached where \(A\)holds, whereas the formula \(\langle (\alpha;\beta)^*\rangle A\) meansthat there is a sequence of alternating executions of \(\alpha\) and\(\beta\) such that a state is reached where \(A\) holds. Semanticallyspeaking, formulas are interpreted by sets of states and programs areinterpreted by binary relations over states in a transition system.More precisely, the meaning of PDL formulas and programs isinterpreted over Labeled Transition Systems (LTS) \(M = (W,R,V)\)where \(W\) is a nonempty set of worlds or states, \(R\) is a mappingfrom the set \(\Pi_0\) of atomic programs into binary relations on\(W\) and \(V\) is a mapping from the set \(\Phi_0\) of atomicformulas into subsets of \(W\).

Informally, the mapping \(R\) assigns to each atomic program\(\pi\in\Pi_0\) some binary relation \(R(\pi)\) on \(W\) with theintended meaning that \(xR(\pi)y\) iff there exists an execution of\(\pi\) from \(x\) that leads to \(y\), whereas the mapping \(V\)assigns to each atomic formula \(p\in\Phi_0\) some subset \(V(p)\) of\(W\) with the intended meaning that \(x \in V(p)\) iff \(p\) is truein the state \(x\). Given our readings of \(0\), \(\lnot A\), \(A\lorB\), \([\alpha]A\), \(\alpha;\beta\), \(\alpha\cup\beta\),\(\alpha^*\) and \(A?\), it is clear that \(R\) and \(V\) must beextended inductively as follows to supply the intended meanings forthe complex programs and formulas:

• \(xR(\alpha;\beta)y\) iff there exists a world \(z\) such that\(xR(\alpha)z\) and \(zR(\beta)y\)
• \(xR(\alpha\cup\beta)y\) iff \(xR(\alpha)y\) or\(xR(\beta)y\)
• \(xR(\alpha^*)y\) iff there exists a non-negative integer \(n\)and there exists a sequence of states \(z_0, \ldots, z_n\) such that\(z_0 = x\), \(z_n = y\) and for all \(k = 1 \ldots n\),\(z_{k-1}R(\alpha)z_k\)
• \(xR(A?)y\) iff \(x = y\) and \(y \in V(A)\)
• \(V(0) = \emptyset\)
• \(V(\lnot A) = W \setminus V(A)\)
• \(V((A\lor B) = V(A) \cup V(B)\)
• \(V([\alpha]A) = \{x \mid \text{for all worlds } y, \text{ if }xR(\alpha)y \text{ then } y \in V(A)\}\)

If \(x \in V(A)\) then we say that \(A\) is satisfied at state \(x\)in \(M\), or \(\ldquo M, x\) sat \(A\rdquo\).

Two Labeled Transition Systems: \(M = (W,R,V)\) (left) and \(M' =(W',R',V')\) (right)

Call \(M\) the LTS depicted above on the left and \(M'\) the LTSdepicted on the right. Defined formally, we have \(M = (W, R, V)\)with \(W = \{x_1,x_2\}\), \(R(\pi_1) = \{(x_1,x_1)\}\), \(R(\pi_2) =\{(x_1,x_2)\}\), \(V(p) = \{x_1\}\), \(V(q) = \{x_2\}\), and we have\(M' = (W',R',V')\) with \(W' = \{y_1, y_2, y_3, y_4\}\), \(R'(\pi_1)= \{(y_1, y_2), (y_2, y_2)\}\), \(R'(\pi_2) = \{(y_1, y_3), (y_2,y_4)\}\), \(V'(p) = \{y_1, y_2\}\), \(V'(q) = \{y_3, y_4\}\). We havefor instance:

• \(M,x_1\) sat \(p\)
• \(M,x_2\) sat \(q\)
• \(M,x_1\) sat \(\langle \pi_1 \rangle p \land \langle \pi_2\rangle q\)
• \(M,x_1\) sat \([\pi_1]p \land [\pi^*_1]p\)
• \(M',y_1\) sat \(\langle \pi^*_1;\pi_2\rangle q\)
• \(M',y_2\) sat \([\pi^*_1] p\)
• \(M',y_1\) sat \([\pi_1 \cup \pi_2] (p \lor q)\)
• \(M',y_3\) sat \([\pi_1 \cup \pi_2] 0\)

Now consider a formula \(A\). We say that \(A\) is valid in \(M\) orthat \(M\) is a model of \(A\), or “\(M \models A\)”, ifffor all worlds \(x\), \(x \in V(A)\). \(A\) is said to be valid, or“\(\models A\)”, iff for all models \(M\), \(M \modelsA\). We 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 \in V(A)\). \(A\) is said to be satisfiable, or“sat \(A\)”, iff there exists a model \(M\) such that\(M\) sat \(A\). It is notably the case that,

sat \(A\) iff not \(\models \lnot A\)
\(\models A\) iff not sat \(\lnot A\)

Some remarkable formulas of PDL are valid. (The reader may try toprove them formally, or at least start convincing themselves on thefew examples displayed above.)

\(\models [\alpha ; \beta]A \leftrightarrow [\alpha][\beta]A\)
\(\models [\alpha \cup \beta]A \leftrightarrow [\alpha]A \land[\beta]A\)
\(\models [\alpha^*]A \leftrightarrow A \land [\alpha][\alpha^*]A\)
\([A?]B \leftrightarrow (A \rightarrow B)\)

Equivalently, we can write them under their dual form.

\(\langle\alpha ; \beta\rangle A \leftrightarrow\langle\alpha\rangle\langle\beta\rangle A\)
\(\langle\alpha \cup \beta\rangle A \leftrightarrow\langle\alpha\rangle A \lor \langle\beta\rangle A\)
\(\langle\alpha^*\rangle A \leftrightarrow A \lor \langle\alpha\rangle\langle\alpha^*\rangle A\)
\(\langle A?\rangle B \leftrightarrow A \land B\)

One interesting notion concerns the information, expressed with PDLformulas, that is contained in an LTS. The behavior of a systemdescribed as an LTS is indeed often slightly hidden in its form. Forinstance, on simple inspection, it is easy to convince oneself thatthe two LTSs depicted above have the same behavior, and satisfy thesame PDL formulas. To finish this section on syntax and semantics wegive the theoretical foundation of these claims.

Given two LTSs, one may ask whether they satisfy the same formulas.The notion of bisimulation has become the standard measure forequivalence of Kripke models and Labeled Transition Systems. Abisimulation between the LTSs \(M = (W,R,V)\) and \(M' =(W',R',V')\) is a binary relation \(Z\) between their set of statessuch that for all worlds \(x\) in \(W\) and for all worlds \(x'\) in\(W'\), if \(xZx'\) then,

• for all atomic formulas \(p\in \Phi_0\), we have \(x\in V(p)\) iff\(x' \in V'(p)\),
• for all atomic programs \(\pi \in \Pi_0\) and for all worlds \(y\in W\), we have that if \(x R(\pi)y\) then there exists a world \(y'\in W'\) such that \(yZy'\) and \(x' R'(\pi)y'\),
• for all atomic programs \(\pi \in \Pi_0\) and for all worlds \(y'\in W'\), we have that if \(x' R'(\pi)y'\) then there exists a world\(y \in W\) such that \(yZy'\) and \(x R(\pi)y\).

We say that two LTSs arebisimilar when there exists abisimulation between them.

It is the case that in two bisimilar LTSs \(M = (W,R,V)\) and \(M' =(W',R',V')\), for all worlds \(x\) in \(W\) and for all worlds \(x'\)in \(W'\), if \(xZx'\) then for all PDL formulas \(A\), \(x \in V(A)\)iff \(x' \in V'(A)\). Thus when two LTSs are bisimilar under thedefinition of bisimulation above, it is the case that, if \(xZx'\)then

• for all programs \(\alpha\) and for all worlds \(y \in W\), wehave that if \(x R(\alpha)y\) then there exists a world \(y' \in W'\)such that \(yZy'\) and \(x' R'(\alpha)y'\),
• for all programs \(\alpha\) and for all worlds \(y' \in W'\), wehave that if \(x' R'(\alpha)y'\) then there exists a world \(y \in W\)such that \(yZy'\) and \(x R(\alpha)y\).

Hence one can simply compare the behaviors of two LTSs by inspectingsolely the atomic programs and safely extrapolate on the comparativebehavior of these LTSs even for complex programs. We say that theprogram constructs of PDL aresafe for bisimulation. See VanBenthem [1998] for precise characterizations of program constructsthat are safe for bisimulation.

It is readily seen that the two instances of LTSs above are bisimilar.A bisimulation \(Z\) between the two models \(M\) and \(M'\) depictedin the figures above can be given as: \(Z = \{(x_1,y_1), (x_1,y_2),(x_2, y_3), (x_2, y_4)\}\). The states \(x_1\) and \(y_1\) satisfyexactly the same PDL formulas. So do the states \(x_1\) and \(y_2\),etc.

2.2 Axiomatization and completeness

The purpose of the proof theory is to provide the characterization ofvalidity—the property \(\models A\)—in terms of axioms andrules of inference. In this section, we define a deducibilitypredicate \(\vdash\) inductively by operations on formulas that dependonly on their syntactic structure in such a way that for all formulas\(A\),

\(\vdash A\) iff \(\models A\).

Of course, PDL is an extension of classical propositional logic. Wefirst expect that all propositional tautologies hold, and allpropositional reasoning is allowed. In particular, modus ponens is avalid rule: from \(A\) and \(A \rightarrow B\) infer \(B\). For anyprogram \(\alpha\), restricting an LTS to the relation \(R(\alpha)\)we obtain a Kripke model in which the logic of the modality\([\alpha]\) is the weakest propositional normal modal logic, namely,the logic K. Thus, PDL contains every instance of the familiardistribution axiom schema

(K)

\([\alpha](A \rightarrow B) \rightarrow ([\alpha]A \rightarrow[\alpha]B)\)

and it is closed under the following rule of inference(necessitation rule)

(N)

from \(A\) infer \([\alpha]A\)

A modal logic is normal if it obeys (K) and (N). An important propertyof normal modal logics is thedistributivity over theconjunction \(\land\): the formula \([\alpha](A \land B)\leftrightarrow ([\alpha]A \land [\alpha]B)\) can be proven using (K),(N), and propositional reasoning. The rule ofmonotony canalso be proven using (K), (N), and propositional reasoning: from \(A\rightarrow B\) infer \([\alpha]A \rightarrow [\alpha]B\).

PDL is the least normal modal logic containing every instance of thefollowing axiom schemas

(A1)

\([\alpha;\beta]A \leftrightarrow [\alpha][\beta]A\)

(A2)

\([\alpha \cup \beta]A \leftrightarrow [\alpha]A \land[\beta]A\)

(A3)

\([\alpha^*]A \leftrightarrow A \land [\alpha][\alpha^*]A\)

(A4)

\([A?]B \leftrightarrow (A \rightarrow B)\)

and closed under the following rule of inference (loopinvariance rule):

(I)

from \(A \rightarrow [\alpha]A\) infer \(A \rightarrow[\alpha^*]A\)

If \(X\) is a set of formulas and \(A\) is a formula then we say that\(A\) is \(\vdash\)-deducible from \(X\), or “\(X \vdashA\)”, if there exists a sequence \(A_0, A_1, \ldots A_n\) offormulas such that \(A_n = A\) and for all \(i \leq n\), \(A_i\) is aninstance of an axiom schema, or a formula of \(X\), or comes fromearlier formulas of the sequence by a rule of inference. Further,\(\vdash A\) iff \(\emptyset \vdash A\); in this case we say that\(A\) is \(\vdash\)-deducible. \(X\) is said to be\(\vdash\)-consistent iff not \(X \vdash 0\). It is easy to establishthat the rule (I) can be replaced by the following axiom schema(induction axiom schema):

(A5)

\(A \land [\alpha^*](A \rightarrow [\alpha]A) \rightarrow[\alpha^*]A\)

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

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

The axiomatization of PDL based on axiom schemas (A1), (A2), (A3),(A4) and (A5) has been proposed in Segerberg [1977]. It is immediatefrom the definitions above that \(\vdash\) is sound with respect to\(\models\), i.e.,

for all formulas \(A\), if \(\vdash A\), then \(\models A\).

The proof proceeds by induction on the length of \(A\)’sdeduction in \(\vdash\). The question of the completeness of\(\vdash\) with respect to \(\models\), i.e.,

for all formulas \(A\), if \(\models A\), then \(\vdash A\),

was pursued by several logicians. The line of reasoning presented inSegerberg [1977] was the first attempt to prove the completeness of\(\vdash\). Soon, Parikh came up with a proof, too. When early 1978Segerberg found a flaw in his argument (which he repaired eventually),Parikh published what can be considered the first proof of thecompleteness of \(\vdash\) in Parikh [1978]. Different proofs ofcompleteness of \(\vdash\) have been published since, e.g. Kozen andParikh [1981]. More details can be found in Pratt [2017].

Different alternative proof theories of PDL have also been soughtafter. Even early on, notably in Pratt [1978]. Let us then alsomention the completeness of related theories by Nishimura [1979] andVakarelov [1983].

An alternative formulation of a deducibility predicate for PDLexploits an infinitary rule of inference, as for instance in Goldblatt[1992a]. (An infinitary rule of inference takes an infinite number ofpremises.) Let \(\vdash'\) be the deducibility predicate correspondingin the language of propositional dynamic logic to the least normalmodal logic containing every instance of the axiom schemas (A1), (A2),(A3) and (A4) and closed under the following infinitary rule ofinference:

(I′)

from \(\{[\beta][\alpha^n]A : n\geq 0\}\) infer\([\beta][\alpha^*]A\)

It can be proved that \(\vdash'\) is both sound and complete withrespect \(\models\), i.e.,

for all formulas \(A\), \(\vdash' A\) iff \(\models A\).

In other words, as far as generating the set of all valid formulas isconcerned, the proof systems \(\vdash\) and \(\vdash'\) areequivalent.

2.3 Decidability and complexity

The aim of the complexity theory is to establish the computability ofthe property sat \(A\) in terms of resources of time or space. Thecomplexity of a logic \(\mathcal{L}\) is often identified with theproblem of deciding the satisfiability of its formulas, definedas:

(L-SAT)

Given a formula \(A\) of \(\mathcal{L}\), is \(A\)satisfiable?

In this section, we investigate the complexity of the followingdecision problem:

(PDL-SAT)

Given a formula \(A\) of PDL, is \(A\) satisfiable?

The complete axiomatization of PDL is a recursive definition of theset of valid PDL formulas, or in other words, of the set of formulaswhose negation is not satisfiable. Hence, concerning the problem(PDL-SAT), we have a sub-procedure that would answer “no”if the PDL formula \(A\) were not satisfiable. The sub-procedure (SP1)consists in enumerating all the formulas \(\vdash\)-deducible,starting from the axioms and inferring other theorems with the help ofthe inference rules. Given enough time, if a formula is\(\vdash\)-deducible, the sub-procedure would find it eventually.Thus, if \(A\) is not satisfiable, (SP1) must eventually find \(\lnotA\), and answer “no” when it does.

However, if the formula \(A\) is satisfiable, then (SP1) would neverfind \(\lnot A\). It would run forever, and one could not be sureabout it at any time. But there is a way out of this uncertainty. Wecan also think of a second sub-procedure that answers“yes” if a PDL formula is satisfiable. Indeed, one of theearliest results on PDL was the proof that PDL has thefinitemodel 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 offers a basis for a sub-procedure (SP2)that consists in enumerating one by one the finite models of PDL andtesting whether one of them satisfies the formula. (For all formulas\(A\) and for all finite models \(M\), it is easy to test if \(M\) sat\(A\) by applying the definition of \(V(A)\).) Thus, if \(A\) issatisfiable, it must eventually find a model \(M\) such that \(M\) sat\(A\), and answer “yes” when it does. Symmetrically to thefirst sub-procedure (SP1), if the formula \(A\) is not satisfiable,then (SP2) will never find a model satisfying it, it will run forever,and one could not be sure about it at any time.

Now, combining (SP1) and (SP2) together we have a way of decidingwhether a PDL formula \(A\) is satisfiable. It suffices to run them inparallel: if \(A\) is satisfiable then (SP2) will eventually answer“yes”, if \(A\) is not satisfiable then (SP1) willeventually answer “no”. The procedure halts when either(SP1) or (SP2) provides an answer.

If the procedure that is obtained is sufficient to conclude that theproblem (PDL-SAT) is decidable, it is very inefficient in practice.There is a result—due to Fischer and Ladner [1979] and Kozen andParikh [1981]— stronger than the finite model property, that issmall model property:

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

This means that we would now know when to stop looking for a modelsatisfying a formula in the procedure (SP2). Hence, we can use (SP2)to test whether a formula is satisfiable, but once we have exhaustedall small models, we can conclude that the formula is not satisfiable.This yields a procedure that runs non-deterministically in exponentialtime (NEXPTIME): guess a model of size at most singly exponential, andcheck whether it satisfies the formula. But the key results in thecomplexity theory of PDL come from Fischer and Ladner [1979] and Pratt[1980a]. Observing that a formula of PDL can efficiently describe thecomputation of a linear space bounded alternating Turing machine,Fischer and Ladner [1979] first established the lower bound ofexponential time of (PDL-SAT). The EXPTIME upper bound of (PDL-SAT)has been obtained by Pratt [1980a], who adapted the method of semantictableaux to PDL. Thus, (PDL-SAT) is EXPTIME-complete. (An algorithmmore efficient in practice, although still running in deterministicexponential time in the worst case, is proposed in De Giacomo andMassacci [2000].)

3. Structured programming and correctness of programs

Historically, logics of programs stem from the work in the late 1960sof computer scientists interested in assigning meaning to programminglanguages and finding a rigorous standard for proofs about theprograms. For example such proofs may be about the correctness of aprogram with respect to an expected behavior, or about the terminationof a program. A seminal paper is Floyd [1967] which presents ananalysis of the properties of structured computer programs usingflowcharts. Some early work such as Yanov [1959] or Engeler[1967] had advanced and studied formal languages in which theproperties of program connectives can be expressed. The formalism ofHoare [1969] was a milestone in the advent of PDL. It was proposed asa rigorous axiomatic interpretation of Floyd’s flowcharts. Weoften talk about Hoare logic, or Floyd-Hoare logic, or Hoare calculuswhen referring to this formalism. Hoare calculus is concerned with thetruth of statements (“Hoare triples”), such as\(\{A\}\alpha\{B\}\) which establishes a connection between aprecondition \(A\), a program \(\alpha\), and a post-condition \(B\).It indicates that whenever \(A\) holds as a precondition of theexecution of \(\alpha\), then \(B\) holds as a post-condition afterthe successful execution of \(\alpha\).

It was true some decades ago, and it is still the case: validating aprogram is more often than not done by testing it on a reasonablevariety of inputs. When an input does not yield the expected output,the “bug” is fixed. If eventually for every tested inputwe obtain the expected output, one has a reasonable belief that theprogram has no error. However, this is a time consuming method ofvalidation, and it leaves place for untested inputs that could fail.Finding these errors after the program has been implemented and goneinto use is even more costly in resources. Reasoning about programcorrectness with formal methods is crucial for critical systems sinceit offers a way of proving exhaustively that a program has noerrors.

3.1 Hoare calculus

To illustrate the sort of principles of programs captured by the rulesin the Hoare calculus it is enough to consult some of them. (N.B.: therules mean that if all the statements above the rule linehold—the premises—then also the statement under the ruleline—the conclusion— holds.)

The rule of composition captures the elementary sequential compositionof programs. As premises, we have two assumptions about the partialcorrectness of two programs \(\alpha_1\) and \(\alpha_2\). The firstassumption is that when \(\alpha_1\) is executed in a state satisfying\(A\), then it will finish in a state satisfying \(B\), whenever ithalts. The second assumption is that when \(\alpha_2\) is executed ina state satisfying \(B\), then it will finish in a state satisfying\(C\), whenever it halts. The conclusion of the rule is about thepartial correctness of the program \(\alpha_1;\alpha_2\) (i.e.,\(\alpha_1\) sequentially composed with \(\alpha_2\)), that followsfrom the two assumptions. Namely, we can conclude that if\(\alpha_1;\alpha_2\) is executed in a state satisfying \(A\), then itfinishes in a state satisfying \(C\), whenever it halts.

The rule of iteration is an important one because it captures theessential ability of programs to execute some portion of coderepeatedly until a certain condition ceases to hold.

Finally, the two rules of consequence are fundamental to give a formalbasis to intuitively clear reasoning involving weaker post-conditionsand stronger preconditions respectively.

From the formalism presented in Hoare [1969], we leave out its axiomschemas as it would require a first-order language. Finally, insubsequent work on Hoare logic, more rules are also often added. SeeApt [1979] for an early overview.

3.2 Hoare calculus and PDL

Dynamic logics come from Pratt’s interpretation of Hoare triplesand Hoare calculus in the formalism of modal logic. With the modality\([\alpha]\), we can express formally that all states reachable byexecuting the program \(\alpha\) satisfy the formula \(A\). This isdone by writing \([\alpha]A\). Thus, the Hoare triple\(\{A\}\alpha\{B\}\) is simply captured by the PDL formula

\(A \rightarrow [\alpha]B\).

In addition, important programming constructs are easily introduced inPDL by definitional abbreviation:

• \(\mathsf{if}~ A ~\mathsf{then}~ \alpha ~\mathsf{else}~ \beta :=((A?;\alpha) \cup (\lnot A?;\beta))\)
• \(\mathsf{while}~ A ~\mathsf{do}~ \alpha := ((A?;\alpha)^*;\lnotA?)\)
• \(\mathsf{repeat}~ \alpha ~\mathsf{until}~ A := (\alpha;((\lnotA;\alpha)^*;A?))\)
• \(\mathsf{abort} := 0?\)
• \(\mathsf{skip} := 1?\)

Thus, it seems that with PDL we are well-equipped to logically provethe correctness of structured programs. Beyond this rather hand-wavingconnection between PDL and Hoare calculus, perhaps it is not yet clearhow they relate formally. PDL is in fact a generalization of Hoarecalculus in the sense that all the rules of the Hoare calculus can beproven in the axiomatic system of PDL. (Rigorously, the Hoare calculuscontains axioms that would require the extended language offirst-order Dynamic Logic.) This is quite remarkable, so we will showhow they can be derived.

The proofs start by assuming the premises of the rules. Then by usingthese assumptions, axioms and rules of PDL, and nothing else, theobjective is to establish that the conclusion of the rules logicallyfollows. Hence, for the rule of composition, we start by assuming\(\{A\}\alpha_1\{B\}\), that is \(A \rightarrow [\alpha_1]B\) in itsPDL formulation, and by assuming \(\{B\}\alpha_2\{C\}\), that is \(B\rightarrow [\alpha_2]C\). The objective is to prove that\(\{A\}\alpha_1;\alpha_2\{C\}\). Precisely, we want to establish that\(A \rightarrow [\alpha_1;\alpha_2]C\) is \(\vdash\)-deducible fromthe set of formulas \(\{A \rightarrow [\alpha_1]B, B \rightarrow[\alpha_2]C\}\).

The proof of the rule of iteration is slightly more involved.

In the context of PDL, the two rules of consequence are in factspecial cases of the rule of composition. To obtain the first rule,substitute \(\alpha_1\) with \(\alpha\) and \(\alpha_2\) with\(\mathsf{skip}\). To obtain the second rule, substitute \(\alpha_1\)with \(\mathsf{skip}\) and \(\alpha_2\) with \(\alpha\). It sufficesto apply the axiom schema (A4), and to remark that\([\alpha;\mathsf{skip}]A \leftrightarrow [\alpha]A\) and\([\mathsf{skip};\alpha]A \leftrightarrow [\alpha]A\) are also\(\vdash\)-deducible for all \(A\) and all \(\alpha\).

3.3 Total correctness

By Hoare’s own admission in Hoare [1979], his original calculuswas merely a starting point and suffered quite a few limitations.Particularly, it only allows one to reason aboutpartialcorrectness. That is, the truth of a statement \(\{A\}\alpha\{B\}\)only makes sure that all executions of \(\alpha\) starting in a statesatisfying \(A\) will end in a state satisfying \(B\),or will nothalt. That is, a partially correct program may havenon-terminating executions. (In fact, a program that has noterminating execution will always be partially correct. This is thecase for example of the program \(\mathsf{while}~ 1 ~\mathsf{do}~\mathsf{skip}\). The formula \(A \rightarrow [\mathsf{while}~1~\mathsf{do} ~\mathsf{skip}] B\) is deducible for all formulas \(A\)and \(B\).) The calculus offers no basis for a proof that a programterminates. It can be modified so as to account fortotalcorrectness of programs: partial correctness plus termination. It isachieved by amending the rule of iteration. We do not present it hereand refer the interested reader to Apt [1981].

Let us first observe that fordeterministic programs, one canalready capture total correctness via formulas of the kind

\(A \rightarrow \langle\alpha\rangle B\).

The expression \(\langle\alpha\rangle B\) means that there is anexecution of \(\alpha\) that terminates in a state that satisfies\(B\). Moreover, if \(\alpha\) is deterministic, this possibleterminating execution is the unique execution of \(\alpha\). Thus, ifone first manages to prove that a program is deterministic, this trickworks well enough to prove its total correctness.

A general solution to the problem of total correctness exists in therealm of PDL. But we need to extend it a little. Pratt had alreadyalluded in Pratt [1980b] that PDL is not expressive enough to capturethe infinite looping of programs. In reaction, PDL with repeating(RPDL) was introduced by Streett [1982]. It contains, for all programs\(\alpha\), the expression \(\Delta\alpha\) standing for a newproposition with semantics:

Streett [1982] conjectured that RPDL can be axiomatized by adding tothe proof system of PDL precisely the following axiom schemas.

(A6)

\(\Delta\alpha \rightarrow \langle\alpha\rangle\Delta\alpha\)

(A7)

\([\alpha^*](A \rightarrow \langle\alpha\rangle A) \rightarrow (A\rightarrow \Delta\alpha)\)

The proof of the conjecture was provided in Sakalauskaite and Valiev[1990]. (A version of the conjecture in the variant of combinatory PDLwas also proved in Gargov and Passy [1988].)

It is easy to see that in the Hoare calculus presented above, nontermination can only come from the rule of iteration. Analogously, nontermination of a PDL program can only come from the use of theunbounded iteration. The expression \(\Delta\alpha\) indicates that\(\alpha^*\) can diverge, and this is just the kind of notion we need.We can now inductively define a predicate \(\infty\) such that for aprogram \(\alpha\), the formula \(\infty(\alpha)\) will be trueexactly when \(\alpha\) can enter a non-terminating computation.

\(\infty(\pi) := 0\) where \(\pi\in\Pi_0\)
\(\infty(A?) := 0\)
\(\infty(\alpha \cup \beta) := \infty(\alpha)\ \lor \infty(\beta)\)
\(\infty(\alpha ; \beta) := \infty(\alpha) \lor \langle\alpha\rangle\infty(\beta)\)
\(\infty(\alpha^*) := \Delta\alpha \lor \langle\alpha^*\rangle\infty(\alpha)\)

Finally, the total correctness of a program can be expressed viaformulas of the kind

\(A \rightarrow (\lnot \infty(\alpha) \land [\alpha]B)\),

which means literally that if \(A\) is the case, then the program\(\alpha\) cannot run forever, and every successful execution of\(\alpha\) will end in a state satisfying \(B\).

4. Some variants

Results concerning comparative power of expression, decidability,complexity, axiomatization and completeness of a number of variants ofPDL obtained by extending or restricting its syntax and its semanticsconstitute the subject of a wealth of literature. We can only say somuch and we will address just a few of these variants leaving out bigchunks of otherwise important work in dynamic logic.

4.1 PDL without tests

The axiom schema \([A?]B \leftrightarrow (A \rightarrow B)\) seems toindicate that for every formula \(C\), there exists an equivalenttest-free formula \(C'\)—i.e., there is a test-free formula\(C'\) such that \(\models C \leftrightarrow C'\). It is interestingto observe that this assertion is untrue. Let PDL₀ be therestriction of PDL to test-free regular programs, i.e., programs whichdo not contain tests. Berman and Paterson [1981] considered the PDLformula \(\langle (p?;\pi)^*;\lnot p?;\pi;p?\rangle 1\), which is

\(\langle \mathsf{while}~ p~ \mathsf{do}~ \pi \rangle \langle \pi\rangle p\),

and proved that there is no PDL₀ formula equivalent to it.Hence, PDL has more expressive power than PDL₀. Theirargument actually can be generalized as follows. For all \(n \geq 0\),let PDL_n+1 be the subset of PDL in which programscan contain tests \(A?\) only if \(A\) is a PDL_nformula. For all \(n \geq 0\), Berman and Paterson considered thePDL_n+1 formula \(A_{n+1}\) defined by

\(\langle \mathsf{while}~ A_n~ \mathsf{do}~ \pi_n\rangle \langle\pi_n\rangle A_n\),

where \(A_0 = p\) and \(\pi_0 = \pi\) and proved that for all \(n \geq0\), there is no PDL_n formula equivalent to\(A_{n+1}\). Hence, for all \(n \geq 0\), PDL_n+1has more expressive power than PDL_n.

4.2 PDL with converse

CPDL is the extension of PDL with converse. It is a construct that hasbeen considered since the beginning of PDL. For all programs\(\alpha\), let \(\alpha^{-1}\) stand for a new program withsemantics

\(xR(\alpha^{-1})y\) iff \(yR(\alpha)x\).

The converse construct allows us to express facts about statespreceding the current one and to reason backward about programs. Forinstance, \([\alpha^{-1}]A\) means that before executing \(\alpha\),\(A\) had to hold. We have

\(\models A \rightarrow [\alpha]\langle \alpha ^{-1}\rangle A\)
\(\models A \rightarrow [\alpha ^{-1}]\langle \alpha \rangle A\)

The addition of the converse construct does not change thecomputational properties of PDL in any significant way. By addingevery instance of the following axiom schemas

(A8)

\(A \rightarrow [\alpha ]\langle \alpha^{-1}\rangle A\)

(A9)

\(A \rightarrow [\alpha^{-1}]\langle \alpha \rangle A\)

to the proof system of PDL, we obtain a sound and completededucibility predicate in the extended language. See Parikh [1978] fordetails. CPDL has the small model property and (CPDL-SAT) isEXPTIME-complete.

It is easy to notice that CPDL has more expressive power than PDL. Tosee this, consider the CPDL formula \(\langle \pi^{-1}\rangle 1\) andthe LTSs \(M = (W, R, V)\) and \(M' = (W', R', V')\) where \(W =\{x,y\}\), \(R(\pi) = \{(x,y)\}\), \(W' = \{y'\}\), \(R'(\pi) =\emptyset\) and \(V(x) = V(y) = V'(y') = \emptyset\). Since \(M, y\)sat \(\langle \pi^{-1}\rangle 1\), not \(M', y'\) sat \(\langle \pi^{-1}\rangle 1\), and because for all PDL formulas \(A\) it is thecase that \(M, y\) sat \(A\) iff \(M', y'\) sat \(A\), then it isclear that no PDL formula is equivalent to \(\langle \pi^{-1}\rangle1\).

4.3 PDL with repeating and looping

We have already exposed the power of repeating insection 3.3 by introducing RPDL. Here, we summarize more results about RPDL andits connection with other variations on the notion of repeatingprograms.

Concerning the complexity theory of RPDL, Streett [1982] had alreadyestablished that RPDL had the finite model property; precisely thatevery RPDL satisfiable formulaA is satisfiable in a model ofsize at most triply exponential in the length ofA. Anautomata-theoretic argument permitted to conclude that the problem(RPDL-SAT) can be solved in deterministic triple exponential time(3-EXPTIME). The gap between this upper bound for deciding (RPDL-SAT)and the simple exponential-time lower bound for deciding (PDL-SAT) wasthus open. The problem found itself greatly connected to the growinginterest of computer scientists in establishing the complexity oftemporal logics, and more specifically of the (propositional) modal\(\mu\)-calculus (MMC) due to Kozen [1983], because RPDL has a linearblow-up translation to MMC. In Vardi and Stockmeyer [1985], an upperbound in non-deterministic exponential time was shown. In Emerson andJutla [1988] and in its final form in Emerson and Jutla [1999], it wasshown that (MMC-SAT) and (RPDL-SAT) are EXPTIME-complete. If we addthe converse operator ofsection 4.2 one obtains CRPDL. The complexity of (CRPDL-SAT) remained open for afew years but it can be shown to be EXPTIME-complete, too. This isachieved by combining the techniques of Emerson and Jutla [1988] andVardi [1985], as in Vardi [1998].

Insection 3.3 we have defined a predicate \(\infty\), where \(\infty(\alpha)\)means that the program \(\alpha\) can have a non-terminatingcomputation. We call LPDL the logic obtained by augmenting PDL withthe predicate \(\infty\). Clearly, RPDL is at least as expressive asLPDL; The inductive definition of \(\infty(\alpha)\) in the languageof RPDL is the witness of it. RPDL is in fact strictly more expressivethan LPDL. This was shown in Harel and Sherman [1982]. As it can besuspected, both RPDL and LPDL have more expressive power than PDL. Itis established by proving that some formulas of RPDL and of LPDL haveno equivalent expression in PDL. The proof involves the technique offiltration which is designed to collapse an LTS to a finitemodel while leaving invariant the truth or falsity of certainformulas. For some set of PDL formulas \(X\), it consists in groupinginto equivalence classes the states of an LTS that satisfy exactly thesame formulas in \(X\). The set of equivalence classes of states thusobtained becomes the set of states of the filtrate model, and atransition is built appropriately over them.

With a carefully chosen set \(FL(A)\) that depends on a PDL formula\(A\) (the so-called Fischer-Ladner closure of the set of sub-formulasof \(A\)), a filtration of an LTS \(M\) yields a finite filtrate model\(M'\), such that \(A\) is satisfiable at a world \(u\) in \(M\) ifand only if it is satisfiable in the equivalence class containing\(u\) in the filtrate. (See Fischer and Ladner [1979].)

We can now consider the filtration of the LTS \(M=(W,R,V)\) suchthat

• \(W = \{(i,j) : j \text{ and } i \text{ integers}, 1 \leq j \leqi\} \cup \{ u \}\)
• \((i,j)R(\pi )(i,j-1)\) when \(1 \leq j \leq i\)
• \(uR(\pi )(i,i)\) for every \(i\)
• \(V(p) = \emptyset\) for every \(p \in \Phi_0\)

In one sentence, what goes on in \(M\) is that from the world \(u\),there is an infinite number of finite \(\pi\)-paths of growing length.We have both \(M, u\) sat \(\lnot\Delta\pi\) and \(M, u\) sat\(\lnot\infty(\pi^*)\). Yet, for every PDL formula \(A\), we will haveboth \(\Delta\pi\) and \(\infty(\pi^*)\) that are satisfied at theequivalence class of \(u\) in the model obtained by filtration of\(M\) with \(FL(A)\). Indeed, the filtration must collapse some statesof \(M\) and create some loops. Thus, there exists no PDL formula thatcan express \(\Delta\pi\) and there exists no PDL formula that canexpress \(\infty(\pi^*)\).

There are other ways of making possible the assertion that a programcan execute forever. For instance, Danecki [1984a] proposed apredicate \(\mathsf{sloop}\) to qualify programs that can enter instrong loops, that is:

\(V(\mathsf{sloop}(\alpha)) = \{x: xR(\alpha)x\}\).

Let us call SLPDL the logic obtained by augmenting PDL with formulas\(\mathsf{sloop}(\alpha)\). RPDL and SLPDL are essentiallyincomparable: the predicate \(\Delta\) is not definable in SLPDL, andthe predicate \(\mathsf{sloop}\) is not definable in RPDL. SLPDL doesnot possess the finite model property. For example, the formula

\([\pi^*](\langle\pi\rangle 1 \land \lnot\mathsf{sloop}(\pi^+))\)

is satisfiable in infinite LTSs only. Nonetheless, Danecki [1984a]established the decidability of (SLPDL-SAT) formulas in deterministicexponential time.

4.4 PDL with intersection

Another construct has been studied: the intersection of programs. Byadding intersection of programs to PDL, we obtain the logic IPDL. InIPDL, for all programs \(\alpha\), \(\beta\), the expression \(\alpha\cap \beta\) stands for a new program with semantics

\(xR(\alpha \cap \beta )y\) iff \(xR(\alpha)y\) and \(xR(\beta)y\).

For instance, the intended reading of \(\langle \alpha \cap \beta\rangle A\) is that if we execute \(\alpha\) and \(\beta\) in thepresent state then there exists a state reachable by both programswhich satisfies \(A\). As a result, we have

\(\models \langle \alpha \cap \beta \rangle A \rightarrow \langle\alpha \rangle A \land \langle \beta \rangle A\),

but, in general, we have

not \(\models \langle \alpha \rangle A \land \langle \beta \rangle A\rightarrow \langle \alpha \cap \beta \rangle A\).

Although the intersection of programs is important in variousapplications of PDL to artificial intelligence and computer science(e.g., in the context of concurrency), the proof theory and thecomplexity theory of PDL with intersection remained unexplored forseveral years. Concerning the complexity theory of IPDL, difficultiesappear when one considers the finite model property. In fact theconstruct \(\mathsf{sloop}(\alpha)\) can be expressed in IPDL. Inpropositional dynamic logic with intersection it is equivalent to\(\langle \alpha \cap 1?\rangle 1\). We can thus adapt the formula ofSLPDL ofsection 4.3, and we have that

\([\pi^*](\langle \pi \rangle 1 \land [\pi^+ \cap 1?]0)\)

is satisfiable in infinite LTSs only. In other words, IPDL does notpossess the finite model property. Danecki [1984b] investigated thecomplexity theory of IPDL and showed that deciding (IPDL-SAT) can bedone in deterministic double exponential time. (A modern proof ispresented in Göller, Lohrey and Lutz [2007].) The complexity gapbetween 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 morethan twenty years. In 2004, Lange [2005] established the lower boundof exponential space of (IPDL-SAT). In 2006, Lange and Lutz [2005]gave a proof of a double exponential-time lower bound of thesatisfiability problem for IPDL without tests by a reduction from theword problem of exponentially space-bounded alternating Turingmachines. In this reduction, the role of the iteration construct isessential since, according to Massacci [2001], the satisfiabilityproblem for iteration-free IPDL without tests is only PSPACE-complete.Adding the converse construct to IPDL, we obtain ICPDL. Thesatisfiability problem of ICPDL has been proved to be2-EXPTIME-complete by Göller, Lohrey and Lutz [2007].

Concerning the proof theory of IPDL, difficulties appear when werealize that no axiom schema, in the language of PDL withintersection, “corresponds” to the semantics \(xR(\alpha\cap \beta)y\) iff \(xR(\alpha)y\) and \(xR(\beta)y\) of the program\(\alpha \cap \beta\). That is, not in the same way for example, thatthe axiom schemas (A1) and (A2) “correspond” to thesemantics of the programs \(\alpha;\beta\) and \(\alpha \cup \beta\),respectively. For this reason, the axiomatization of PDL withintersection was open until the complete proof system developed inBalbiani and Vakarelov [2003].

In another variant of PDL, due to Peleg [1987] and further studied byGoldblatt [1992b], the expression \(\alpha \cap \beta\) is interpreted“do \(\alpha\) and \(\beta\) in parallel”. In thiscontext, the binary relations \(R(\alpha)\) and \(R(\beta)\) are nolonger sets of pairs of the form \((x,y)\) with \(x\) and \(y\)worlds, but rather sets of pairs of the form \((x, Y)\) with \(x\) aworld and \(Y\) a set of worlds. It was inspired by the Game Logic ofParikh [1985], an intepretation of PDL with “programs asgames”. Game Logic provides an additional program construct thatdualizes programs, thus permitting to define the intersection ofprograms as the dual of the non-deterministic choice betweenprograms.

5. Conclusion

This article has focused on propositional dynamic logic and some ofits significant variants. There are by now a number ofbooks—Goldblatt [1982], Goldblatt [1992a], Harel [1979] andHarel, Kozen and Tiuryn [2000]—and survey papers—Harel[1984], Kozen and Tiuryn [1990], Parikh [1983] —treating PDL andrelated formalisms. Pratt offers in Pratt [2017] an informal andpersonal perspective on the development of dynamics logics which alsohas a historical value. The body of research on PDL is certainlyinstrumental in developing many logical theories of system dynamics.However, these theories are arguably out of the scope of the presentarticle. Van Eijck and Stokhof [2006] is a more recent overview oftopics making use of dynamic logic, addressing various themes that areof certain interest for philosophers: e.g., dynamics of communication,or natural language semantics. Recent books are going in much detailson newer topics, such as dynamic logic of knowledge (dynamic epistemiclogic) in Van Ditmarsch, Van Der Hoek and Kooi [2007], and the dynamiclogic of continuous and hybrid systems (differential dynamic logic) inPlatzer [2010]. PDL was conceived primarily for reasoning aboutprograms. There are many other applications of modal logic to thereasoning about programs. Algorithmic logic is closer to PDL since itallows one to talk explicitly about programs. The reader is invited toconsult the work presented in Mirkowska and Salwicki [1987]. Temporallogics are now the chief logics in theoretical computer science andhave a close connection with logics of programs. They allow one toexpress the temporal behavior of transition systems with a languagethat abstracts away from the labels (hence the programs). See forinstance Schneider [2004] for an overview of the foundations in thisresearch area.

Bibliography

• Apt, K., 1981, “Ten years of Hoare’s logic: A survey— Part I”,ACM Transactions on Programming Languagesand Systems, 3(4): 431–483.
• Balbiani, P., and D. Vakarelov, 2003, “PDL with intersectionof programs: a complete axiomatization”,Journal of AppliedNon-Classical Logics, 13: 231-276.
• van Benthem, J., 1998, “Program constructions that are safefor bisimulation”,Studia Logica, 60:311–330.
• Berman, F., and M. Paterson, 1981, “Propositional dynamiclogic is weaker without tests”,Theoretical ComputerScience, 16: 321–328.
• Burstall, R., 1974, “Program Proving as Hand Simulation witha Little Induction”,Information Processing 74: Proceedingsof IFIP Congress 74, Amsterdam: North Holland Publishing Company,308–312.
• Danecki, R., 1984a, “Propositional dynamic logic with strongloop predicate”, in M. Chytil and V. Koubek,MathematicalFoundations of Computer Science, Berlin: Springer-Verlag,573-581.
• –––, 1984b, “Nondeterministicpropositional dynamic logic with intersection is decidable”, inA. Skowron (ed.),Computation Theory, Berlin:Springer-Verlag, 34-53.
• De Giacomo, G., and F. Massacci, 2000, “Combining deductionand model checking into tableaux and algorithms forconverse-PDL”,Information and Computation, 160:109–169.
• van Ditmarsch, H., W. van Der Hoek, and B. Kooi, 2007,Dynamicepistemic logic, Dordrecht: Springer-Verlag.
• van Eijck, J., and M. Stokhof, 2006, “The Gamut of DynamicLogics”, in D. Gabbay and J. Woods (eds.),The Handbook ofHistory of Logic, Volume 7—Logic and the Modalities inthe Twentieth Century, Amsterdam: Elsevier, 499–600.
• Emerson, E., and Jutla, C., 1988, “The Complexity of TreeAutomata and Logics of Programs (Extended Abstract)”, inProceedings of the 29th Annual Symposium on Foundations ofComputer Science, Los Alamitos, CA: IEEE Computer Society,328–337.
• –––, 1999, “The Complexity of TreeAutomata and Logics of Programs”, inSIAM Journal ofComputing, 29: 132–158.
• Engeler, E., 1967, “Algorithmic properties ofstructures”,Mathematical Systems Theory, 1:183–195.
• Fischer, M., and R. Ladner, 1979, “Propositional dynamiclogic of regular programs”,Journal of Computer and SystemSciences, 18: 194–211.
• Floyd, R., 1967, “Assigning meaning to programs”,Proceedings of the American Mathematical Society Symposia onApplied Mathematics (Volume 19), Providence, RI: AmericanMathematical Society, 19–31.
• Gargov, G., and S. Passy, 1988, “Determinism and looping incombinatory PDL”,Theoretical Computer Science,Amsterdam: Elsevier, 259–277.
• Goldblatt, R., 1982,Axiomatising the Logic of ComputerProgramming, Berlin: Springer-Verlag.
• –––, 1992a,Logics of Time andComputation, Stanford: Center for the Study of Language andInformation Publications.
• –––, 1992b, “Parallel Action: ConcurrentDynamic Logic with Independent Modalities”,StudiaLogica, 51: 551–578.
• Göller, S., M. Lohrey, and C. Lutz, 2007, “PDL withintersection and converse is 2EXP-complete”,Foundations ofSoftware Science and Computational Structures, Berlin: Springer,198–212.
• Harel, D., 1979,First-Order Dynamic Logic, Berlin:Springer-Verlag.
• –––, 1983, “Recurring dominoes: making thehighly 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 PhilosophicalLogic (Volume II), Dordrecht: D. Reidel, 497–604.
• Harel, D., D. Kozen, and J. Tiuryn, 2000,Dynamic Logic,Cambridge, MA: MIT Press.
• Harel, D. and Sherman, R., 1982, “Looping vs. Repeating inDynamic Logic”,Information and Control, 55:175–192.
• Hoare, C., 1969, “An axiomatic basis for computerprogramming”,Communications of the Association of ComputingMachinery, 12: 576–580.
• Kozen, D., 1983, “Results on the Propositionalμ-Calculus”,Theoretical Computer Science, 27:333–354.
• Kozen, D., and R. Parikh, 1981, “An elementary proof of thecompleteness 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 ComputerScience (Volume B), Amsterdam: Elsevier, 789–840.
• Lange, M., 2005, “A lower complexity bound for propositionaldynamic logic with intersection”, in R. Schmidt, I.Pratt-Hartmann, M. Reynolds and H. Wansing (eds.),Advances inModal Logic (Volume 5), London: King’s CollegePublications, 133–147.
• Lange, M., and C. Lutz, 2005, “2-EXPTIME lower bounds forpropositional dynamic logics with intersection”,Journal ofSymbolic Logic, 70: 1072–1086.
• Lutz, C., 2005, “PDL with intersection and converse isdecidable”. In L. Ong (ed.),Computer Science Logic,Berlin: Springer-Verlag, 413-427.
• Massacci, F., 2001, “Decision procedures for expressivedescription logics with intersection, composition, converse of rolesand role identity”, in B. Nebel (ed.),17th InternationalJoint 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 propositionaldynamic logic”,Acta Informatica, 12:377–400.
• Parikh, R., 1978, “The completeness of propositional dynamiclogic”, in J. Winkowski (ed.),Mathematical Foundations ofComputer Science, Berlin: Springer-Verlag, 1978, 403-415.
• –––, 1983, “Propositional logics ofprograms: new directions”, in M. Karpinski (ed.),Foundations of Computation Theory, Berlin: Springer-Verlag,347-359.
• –––, 1985, “The logic of games and itsapplications”,Annals of Discrete Mathematics, 24:111–140.
• Peleg, D., 1987, “Concurrent dynamic logic”,Journal of the Association of Computing Machinery, 34:450–479.
• Platzer, A., 2010,Logical Analysis of Hybrid Systems: ProvingTheorems for Complex Dynamics, Berlin: Springer, 2010.
• Pratt, V., 1976, “Semantical considerations on Floyd-Hoarelogic”, inProceedings of the 17th IEEE Symposium onFoundations of Computer Science, Los Alamitos, CA: IEEE ComputerSociety, 109–121.
• –––, 1978, “A practical decision methodfor propositional dynamic logic”, inProceedings of the 10thAnnual ACM Symposium on Theory of Computing, New York, NY: ACM,326–337.
• –––, 1980a, “A near-optimal method forreasoning about action”,Journal of Computer and SystemSciences, 20: 231–254.
• –––, 1980b, “Application of Modal Logic toProgramming”,Studia Logica, 39: 257–274.
• –––, 2017, “Dynamic Logic: A PersonalPerspective”,Lecture Notes in Computer Science (Volume10669), Cham: Springer, 153–170.
• Sakalauskaite, J., and M. Valiev, 1990, “Completeness ofpropositional dynamic logic with infinite repeating”, in P.Petkov (ed.),Mathematical Logic, New York: Plenum Press,339–349.
• Salwicki, A., 1970, “Formalized algorithmiclanguages”,Bulletin de l’Academie Polonaise desSciences, Serie des sciences mathematiques, astronomiques etphysiques, 18: 227–232.
• Segerberg, K., 1977, “A completeness theorem in the modallogic of programs”,Notices of the American MathematicalSociety, 24: 522.
• Schneider, K., 2004,Verification of Reactive Systems,Berlin: Springer-Verlag.
• Streett, R., 1982, “Propositional dynamic logic of loopingand converse is elementary decidable”,Information andControl, 54: 121–141.
• Vakarelov, D., 1983, “Filtration theorem for dynamicalgebras with tests and inverse operator”, in A. Salwicki (ed.),Logics of Programs and their Applications, Berlin:Springer-Verlag, 314–324.
• Vardi, M., 1985, “The Taming of Converse: Reasoning aboutTwo-way Computations”, inLecture Notes in ComputerScience (Volume 193), Berlin-Heidelberg: Springer,413–423.
• –––, 1998, “Reasoning about the past withtwo-way automata”, inLecture Notes in Computer Science(Volume 1443), Berlin-Heidelberg: Springer, 628–641.
• Vardi, M., and Stockmeyer, L., 1985, “Improved Upper andLower Bounds for Modal Logics of Programs: Preliminary Report”,inProceedings of the 17th Annual ACM Symposium on Theory ofComputing, New York, NY: ACM, 240–251.
• 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 theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

computability and complexity |computer science, philosophy of |logic: action |logic: and information |logic: modal |logic: temporal