# Dynamic logic (modal logic)

{{#invoke:Hatnote|hatnote}}

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.

## Derivations

The modal logic axiom $[a]p\equiv \neg \langle a\rangle \neg p\,\!$ permits the derivation of the following six theorems corresponding to the above:

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 $p\to q\,\!$ asserts that if $p\,\!$ is true then so is $q\,\!$ , the inference $p\vdash q\,\!$ asserts that if $p\,\!$ is valid then so is $q\,\!$ . 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 $p\vdash [a]p\,\!$ , for example, is sound because its premise asserts that $p\,\!$ holds at all times, whence no matter where $a\,\!$ might take us, $p\,\!$ will be true there. The implication $p\to [a]p\,\!$ is not valid, however, because the truth of $p\,\!$ at the present moment is no guarantee of its truth after performing $a\,\!$ . For example, $p\to [a]p\,\!$ will be true in any situation where $p\,\!$ is false, or in any situation where $[a]p\,\!$ is true, but the assertion $(x=1)\to [x:=x+1](x=1)\,\!$ is false in any situation where $x\,\!$ 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 $k\,\!$ for the action of kicking the TV, and $b\,\!$ for the proposition that the TV is broken, dynamic logic expresses this inference as $b\to [k]b\vdash b\to [k*]b\,\!$ , having as premise $b\to [k]b\,\!$ and as conclusion $b\to [k*]b\,\!$ . The meaning of $[k]b\,\!$ is that it is guaranteed that after kicking the TV, it is broken. Hence the premise $b\to [k]b\,\!$ means that if the TV is broken, then after kicking it once it will still be broken. $k*\,\!$ denotes the action of kicking the TV zero or more times. Hence the conclusion $b\to [k*]b\,\!$ 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 $b\to [k]b\vdash b\to [k*]b\,\!$ is sound. However the implication $(b\to [k]b)\to (b\to [k*]b)\,\!$ is not valid because we can easily find situations in which $b\to [k]b\,\!$ holds but $b\to [k*]b\,\!$ does not. In any such counterexample situation, $b\,\!$ must hold but $[k*]b\,\!$ must be false, while $[k]b\,\!$ 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 $b\to [k]b\,\!$ hold now, whereas the inference succeeds (is sound) because it requires that $b\to [k]b\,\!$ hold in all situations, not just the present one.

## Assignment

The general form of an assignment statement is $x:=e\,\!$ where $x\,\!$ is a variable and $e\,\!$ 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.

An example illustrating assignment in combination with $*\,\!$ is the proposition $\langle (x:=x+1)*\rangle x=7\,\!$ . This asserts that it is possible, by incrementing $x\,\!$ sufficiently often, to make $x\,\!$ equal to 7. This of course is not always true, e.g. if $x\,\!$ is 8 to begin with, or 6.5, whence this proposition is not a theorem of dynamic logic. If $x\,\!$ is of type integer however, then this proposition is true if and only if $x\,\!$ is at most 7 to begin with, that is, it is just a roundabout way of saying $x\leq 7\,\!$ .

With the opaque modalities now out of the way, we can safely substitute $0\,\!$ for $n\,\!$ in the usual manner of first-order logic to obtain Peano's celebrated axiom $(\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!$ , namely mathematical induction.

One subtlety we glossed over here is that $\forall i\,\!$ should be understood as ranging over the natural numbers, where $i\,\!$ is the superscript in the expansion of $a*\,\!$ as the union of $a^{i}\,\!$ over all natural numbers $i\,\!$ . The importance of keeping this typing information straight becomes apparent if $n\,\!$ 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 $n\,\!$ is a real variable and $\Phi (n)\,\!$ is the predicate $n\,\!$ is a natural number, then axiom A6 after the first two substitutions, that is, $(\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!$ , is just as valid, that is, true in every state regardless of the value of $n\,\!$ in that state, as when $n\,\!$ is of type natural number. If in a given state $n\,\!$ is a natural number, then the antecedent of the main implication of A6 holds, but then $n+i\,\!$ is also a natural number so the consequent also holds. If $n\,\!$ 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 $p\land [a*](p\to [a]p)\equiv [a*]p\,\!$ 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

The construct while p do a is realized as $(p?;a)*;\neg p?\,\!$ . This performs $p?;a\,\!$ zero or more times and then performs $\neg p?\,\!$ . As long as $p\,\!$ remains true, the $\neg p?\,\!$ at the end blocks the performer from terminating the iteration prematurely, but as soon as it becomes false, further iterations of the body $p\,\!$ are blocked and the performer then has no choice but to exit via the test $\neg p?\,\!$ .

## 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 $[x:=x+1](x\geq 4)\,\!$ contains all three types: $x\,\!$ , $x+1\,\!$ , and $4\,\!$ are data, $x:=x+1\,\!$ is an action, and $x\geq 4\,\!$ and $[x:=x+1](x\geq 4)\,\!$ 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 $x:=x+1\,\!$ 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 $p\{a\}q\,\!$ as $p\to [a]q\,\!$ . The approach was later published in 1976 as a logical system in its own right. The system parallels A. Salwicki's system of Algorithmic Logic and Edsger Dijkstra's notion of weakest-precondition predicate transformer $wp(a,p)\,\!$ , with $[a]p\,\!$ corresponding to Dijkstra's $wlp(a,p)\,\!$ , 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.