Dynamic Logic (modal Logic) - The Concurrency Challenge

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.