Dynamic logic (modal logic)

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general complex behaviors arising in linguistics, philosophy, AI, and other fields.
Language.
Modal logic is characterized by the modal operators formula_1 (box p) asserting that formula_2 is necessarily the case, and formula_3 (diamond p) asserting that formula_2 is possibly the case. Dynamic logic extends this by associating to every action formula_5 the modal operators formula_6 and formula_7, thereby making it a multimodal logic. The meaning of formula_8 is that after performing action formula_5 it is necessarily the case that formula_2 holds, that is, formula_5 must bring about formula_2. The meaning of formula_13 is that after performing formula_5 it is possible that formula_2 holds, that is, formula_5 might bring about formula_2. These operators are related by formula_18 and formula_19, analogously to the relationship between the universal (formula_20) and existential (formula_21) quantifiers.
Dynamic logic permits compound actions built up from smaller actions. While the basic control operators of any programming language could be used for this purpose, Kleene's regular expression operators are a good match to modal logic. Given actions formula_5 and formula_23, the compound action formula_24, "choice", also written formula_25 or formula_26, is performed by performing one of formula_5 or formula_23. The compound action formula_29, "sequence", is performed by performing first formula_5 and then formula_23. The compound action formula_32, "iteration", is performed by performing formula_5 zero or more times, sequentially. The constant action formula_34 or BLOCK does nothing and does not terminate, whereas the constant action formula_35 or SKIP or NOP, definable as formula_36, does nothing but does terminate.
Axioms.
These operators can be axiomatized in dynamic logic as follows, taking as already given a suitable axiomatization of modal logic including such axioms for modal operators as the above-mentioned axiom formula_18 and the two inference rules "modus ponens" (formula_38 and formula_39 implies formula_40) and "necessitation" (formula_38 implies formula_42).
A1. formula_43
A2. formula_44
A3. formula_45
A4. formula_46
A5. formula_47
A6. formula_48
Axiom A1 makes the empty promise that when BLOCK terminates, formula_2 will hold, even if formula_2 is the proposition false. (Thus BLOCK abstracts the essence of the action of hell freezing over.)
A2 says that NOP acts as the identity function on propositions, that is, it transforms formula_2 into itself.
A3 says that if doing one of formula_5 or formula_23 must bring about formula_2, then formula_5 must bring about formula_2 and likewise for formula_23, and conversely.
A4 says that if doing formula_5 and then formula_23 must bring about formula_2, then formula_5 must bring about a situation in which formula_23 must bring about formula_2.
A5 is the evident result of applying A2, A3 and A4 to the equation formula_64 of Kleene algebra.
A6 asserts that if formula_2 holds now, and no matter how often we perform formula_5 it remains the case that the truth of formula_2 after that performance entails its truth after one more performance of formula_5, then formula_2 must remain true no matter how often we perform formula_5. A6 is recognizable as mathematical induction with the action n := n+1 of incrementing n generalized to arbitrary actions formula_5.
Derivations.
The modal logic axiom formula_72 permits the derivation of the following six theorems corresponding to the above:
T1. formula_73
T2. formula_74
T3. formula_75
T4. formula_76
T5. formula_77
T6. formula_78
T1 asserts the impossibility of bringing anything about by performing BLOCK.
T2 notes again that NOP changes nothing, bearing in mind that NOP is both deterministic and terminating whence formula_79 and formula_80 have the same force.
T3 says that if the choice of formula_5 or formula_23 could bring about formula_2, then either formula_5 or formula_23 alone could bring about formula_2.
T4 is just like A4.
T5 is explained as for A5.
T6 asserts that if it is possible to bring about formula_2 by performing formula_5 sufficiently often, then either formula_2 is true now or it is possible to perform formula_5 repeatedly to bring about a situation where formula_2 is (still) false but one more performance of formula_5 could bring about formula_2.
Box and diamond are entirely symmetric with regard to which one takes as primitive. An alternative axiomatization would have been to take the theorems T1-T6 as axioms, from which we could then have derived A1-A6 as theorems.
The difference between implication and inference is the same in dynamic logic as in any other logic: whereas the implication formula_94 asserts that if formula_2 is true then so is formula_96, the inference formula_97 asserts that if formula_2 is valid then so is formula_96. However the dynamic nature of dynamic logic moves this distinction out of the realm of abstract axiomatics into the common-sense experience of situations in flux. The inference rule formula_100, for example, is sound because its premise asserts that formula_2 holds at all times, whence no matter where formula_5 might take us, formula_2 will be true there. The implication formula_104 is not valid, however, because the truth of formula_2 at the present moment is no guarantee of its truth after performing formula_5. For example, formula_104 will be true in any situation where formula_2 is false, or in any situation where formula_8 is true, but the assertion formula_110 is false in any situation where formula_111 has value 1, and therefore is not valid.
Derived rules of inference.
As for modal logic, the inference rules "modus ponens" and "necessitation" suffice also for dynamic logic as the only primitive rules it needs, as noted above. However, as usual in logic, many more rules can be derived from these with the help of the axioms. An example instance of such a derived rule in dynamic logic is that if kicking a broken TV once can't possibly fix it, then repeatedly kicking it can't possibly fix it either. Writing formula_112 for the action of kicking the TV, and formula_23 for the proposition that the TV is broken, dynamic logic expresses this inference as formula_114, having as premise formula_115 and as conclusion formula_116. The meaning of formula_117 is that it is guaranteed that after kicking the TV, it is broken. Hence the premise formula_115 means that if the TV is broken, then after kicking it once it will still be broken. formula_119 denotes the action of kicking the TV zero or more times. Hence the conclusion formula_116 means that if the TV is broken, then after kicking it zero or more times it will still be broken. For if not, then after the second-to-last kick the TV would be in a state where kicking it once more would fix it, which the premise claims can never happen under any circumstances.
The inference formula_114 is sound. However the implication formula_122 is not valid because we can easily find situations in which formula_115 holds but formula_116 does not. In any such counterexample situation, formula_23 must hold but formula_126 must be false, while formula_117 however must be true. But this could happen in any situation where the TV is broken but can be revived with two kicks. The implication fails (is not valid) because it only requires that formula_115 hold now, whereas the inference succeeds (is sound) because it requires that formula_115 hold in all situations, not just the present one.
An example of a valid implication is the proposition formula_130. This says that if formula_111 is greater or equal to 3, then after incrementing formula_111, formula_111 must be greater or equal to 4. In the case of deterministic actions formula_5 that are guaranteed to terminate, such as formula_135, "must" and "might" have the same force, that is, formula_6 and formula_7 have the same meaning. Hence the above proposition is equivalent to formula_138 asserting that if formula_111 is greater or equal to 3 then after performing formula_135, formula_111 might be greater or equal to 4.
Assignment.
The general form of an assignment statement is formula_142 where formula_111 is a variable and formula_144 is an expression built from constants and variables with whatever operations are provided by the language, such as addition and multiplication. The Hoare axiom for assignment is not given as a single axiom but rather as an axiom schema.
A7. formula_145
This is a schema in the sense that formula_146 can be instantiated with any formula formula_147 containing zero or more instances of a variable formula_111. The meaning of formula_149 is formula_147 with those occurrences of formula_111 that occur free in formula_147, i.e. not bound by some quantifier as in formula_153, replaced by formula_144. For example, we may instantiate A7 with formula_155, or with formula_156. Such an axiom schema allows infinitely many axioms having a common form to be written as a finite expression connoting that form.
The instance formula_157 of A7 allows us to calculate mechanically that the example formula_158 encountered a few paragraphs ago is equivalent to formula_159, which in turn is equivalent to formula_160 by elementary algebra.
An example illustrating assignment in combination with formula_161 is the proposition formula_162. This asserts that it is possible, by incrementing formula_111 sufficiently often, to make formula_111 equal to 7. This of course is not always true, e.g. if formula_111 is 8 to begin with, or 6.5, whence this proposition is not a theorem of dynamic logic. If formula_111 is of type integer however, then this proposition is true if and only if formula_111 is at most 7 to begin with, that is, it is just a roundabout way of saying formula_168.
Mathematical induction can be obtained as the instance of A6 in which the proposition formula_2 is instantiated as formula_170, the action formula_5 as formula_172, and formula_173 as formula_34. The first two of these three instantiations are straightforward, converting A6 to formula_175. However, the ostensibly simple substitution of formula_34 for formula_173 is not so simple as it brings out the so-called "referential opacity" of modal logic in the case when a modality can interfere with a substitution.
When we substituted formula_170 for formula_2, we were thinking of the proposition symbol formula_2 as a rigid designator with respect to the modality formula_181, meaning that it is the same proposition after incrementing formula_173 as before, even though incrementing formula_173 may impact its truth. Likewise, the action formula_5 is still the same action after incrementing formula_173, even though incrementing formula_173 will result in its executing in a different environment. However, formula_173 itself is not a rigid designator with respect to the modality formula_181; if it denotes 3 before incrementing formula_173, it denotes 4 after. So we can't just substitute formula_34 for formula_173 everywhere in A6.
One way of dealing with the opacity of modalities is to eliminate them. To this end, expand formula_192 as the infinite conjunction formula_193, that is, the conjunction over all formula_194 of formula_195. Now apply A4 to turn formula_195 into formula_197, having formula_194 modalities. Then apply Hoare's axiom formula_194 times to this to produce formula_200, then simplify this infinite conjunction to formula_201. This whole reduction should be applied to both instances of formula_202 in A6, yielding formula_203. The remaining modality can now be eliminated with one more use of Hoare's axiom to give formula_204.
With the opaque modalities now out of the way, we can safely substitute formula_34 for formula_173 in the usual manner of first-order logic to obtain Peano's celebrated axiom formula_207, namely mathematical induction.
One subtlety we glossed over here is that formula_208 should be understood as ranging over the natural numbers, where formula_194 is the superscript in the expansion of formula_32 as the union of formula_211 over all natural numbers formula_194. The importance of keeping this typing information straight becomes apparent if formula_173 had been of type "integer", or even "real", for any of which A6 is perfectly valid as an axiom. As a case in point, if formula_173 is a real variable and formula_170 is the predicate formula_173 "is a natural number", then axiom A6 after the first two substitutions, that is, formula_217, is just as valid, that is, true in every state regardless of the value of formula_173 in that state, as when formula_173 is of type "natural number". If in a given state formula_173 is a natural number, then the antecedent of the main implication of A6 holds, but then formula_221 is also a natural number so the consequent also holds. If formula_173 is not a natural number, then the antecedent is false and so A6 remains true regardless of the truth of the consequent. We could strengthen A6 to an equivalence formula_223 without impacting any of this, the other direction being provable from A5, from which we see that if the antecedent of A6 does happen to be false somewhere, then the consequent "must" be false.
Test.
Dynamic logic associates to every proposition formula_2 an action formula_225 called a test. When formula_2 holds, the test formula_225 acts as a NOP, changing nothing while allowing the action to move on. When formula_2 is false, formula_225 acts as BLOCK. Tests can be axiomatized as follows.
A8. formula_230
The corresponding theorem for formula_231 is:
T8. formula_232
The construct if p then a else b is realized in dynamic logic as formula_233. This action expresses a guarded choice: if formula_2 holds then formula_235 is equivalent to formula_5, whereas formula_237 is equivalent to BLOCK, and formula_238 is equivalent to formula_5. Hence when formula_2 is true the performer of the action can only take the left branch, and when formula_2 is false the right.
The construct while p do a is realized as formula_242. This performs formula_235 zero or more times and then performs formula_244. As long as formula_2 remains true, the formula_244 at the end blocks the performer from terminating the iteration prematurely, but as soon as it becomes false, further iterations of the body formula_2 are blocked and the performer then has no choice but to exit via the test formula_244.
Quantification as random assignment.
The random-assignment statement formula_249 denotes the nondeterministic action of setting formula_111 to an arbitrary value. formula_251 then says that formula_2 holds no matter what you set formula_111 to, while formula_254 says that it is possible to set formula_111 to a value that makes formula_2 true. formula_257 thus has the same meaning as the universal quantifier formula_153, while formula_259 similarly corresponds to the existential quantifier formula_260. That is, first-order logic can be understood as the dynamic logic of programs of the form formula_249.
Dijkstra claimed to show the impossibility of a program that sets the value of variable x to an arbitrary positive integer. However, in dynamic logic with assignment and the * operator, x can be set to an arbitrary positive integer with the dynamic logic program formula_262: hence we must either reject Dijkstra's argument or hold that the * operator is not effective.
Possible-world semantics.
Modal logic is most commonly interpreted in terms of possible world semantics or Kripke structures. This semantics carries over naturally to dynamic logic by interpreting worlds as states of a computer in the application to program verification, or states of our environment in applications to linguistics, AI, etc. One role for possible world semantics is to formalize the intuitive notions of truth and validity, which in turn permit the notions of soundness and completeness to be defined for axiom systems. An inference rule is sound when validity of its premises implies validity of its conclusion. An axiom system is sound when all its axioms are valid and its inference rules are sound. An axiom system is complete when every valid formula is derivable as a theorem of that system. These concepts apply to all systems of logic including dynamic logic.
Propositional dynamic logic (PDL).
Ordinary or first-order logic has two types of terms, respectively assertions and data. As can be seen from the examples above, dynamic logic adds a third type of term denoting actions. The dynamic logic assertion formula_263 contains all three types: formula_111, formula_265, and formula_266 are data, formula_267 is an action, and formula_268 and formula_263 are assertions. Propositional logic is derived from first-order logic by omitting data terms and reasons only about abstract propositions, which may be simple propositional variables or atoms or compound propositions built with such logical connectives as "and", "or", and "not".
Propositional dynamic logic, or PDL, was derived from dynamic logic in 1977 by Michael J. Fischer and Richard Ladner. PDL blends the ideas behind propositional logic and dynamic logic by adding actions while omitting data; hence the terms of PDL are actions and propositions. The TV example above is expressed in PDL whereas the next example involving formula_267 is in first-order DL. PDL is to (first-order) dynamic logic as propositional logic is to first-order logic.
Fischer and Ladner showed in their 1977 paper that PDL satisfiability was of computational complexity at most nondeterministic exponential time, and at least deterministic exponential time in the worst case. This gap was closed in 1978 by Vaughan Pratt who showed that PDL was decidable in deterministic exponential time. In 1977, Krister Segerberg proposed a complete axiomatization of PDL, namely any complete axiomatization of modal logic K together with axioms A1-A6 as given above. Completeness proofs for Segerberg's axioms were found by Gabbay (unpublished note), Parikh (1978), Pratt (1979), and Kozen and Parikh (1981).
History.
Dynamic logic was developed by Vaughan Pratt in 1974 in notes for a class on program verification as an approach to assigning meaning to Hoare logic by expressing the Hoare formula formula_271 as formula_272. The approach was later published in 1976 as a logical system in its own right. The system parallels 
Andrzej Salwicki's system of algorithmic logic and Edsger Dijkstra's notion of weakest-precondition predicate transformer formula_273, with formula_8 corresponding to Dijkstra's formula_275, weakest liberal precondition. Those logics however made no connection with either modal logic, Kripke semantics, regular expressions, or the calculus of binary relations; dynamic logic therefore can be viewed as a refinement of algorithmic logic and predicate transformers that connects them up to the axiomatics and Kripke semantics of modal logic as well as to the calculi of binary relations and regular expressions.
The concurrency challenge.
Hoare logic, algorithmic logic, weakest preconditions, and dynamic logic are all well suited to discourse and reasoning about sequential behavior. Extending these logics to concurrent behavior however has proved problematic. There are various approaches but all of them lack the elegance of the sequential case. In contrast Amir Pnueli's 1977 system of temporal logic, another variant of modal logic sharing many common features with dynamic logic, differs from all of the above-mentioned logics by being what Pnueli has characterized as an "endogenous" logic, the others being "exogenous" logics. By this Pnueli meant that temporal logic assertions are interpreted within a universal behavioral framework in which a single global situation changes with the passage of time, whereas the assertions of the other logics are made externally to the multiple actions about which they speak. The advantage of the endogenous approach is that it makes no fundamental assumptions about what causes what as the environment changes with time. Instead a temporal logic formula can talk about two unrelated parts of a system, which because they are unrelated tacitly evolve in parallel. In effect ordinary logical conjunction of temporal assertions is the concurrent composition operator of temporal logic. The simplicity of this approach to concurrency has resulted in temporal logic being the modal logic of choice for reasoning about concurrent systems with its aspects of synchronization, interference, independence, deadlock, livelock, fairness, etc.
These concerns of concurrency would appear to be less central to linguistics, philosophy, and artificial intelligence, the areas in which dynamic logic is most often encountered nowadays.
For a comprehensive treatment of dynamic logic see the book by David Harel et al. cited below.