Dynamic logic
|
|
In digital electronics, dynamic logic is sometimes used to refer to a class of design assumptions more commonly known as clocked logic, used to distinguish this type of logic from static logic. This article is not about that, but instead about the family of modal logics.
Dynamic logic is a kind of multi-modal logic introduced by Vaughan Pratt in the 1970s to reason about programs. The key idea is that programs can be represented by means of an algebra of actions, each of whose elements determine two dual modalities: action a gives a "box" modality [a], and a diamond modality <a>.
The effects of the actions can then be captured by means of axioms which determine the meaning of complex actions according to the scheme:
- <a>P is true if P could be true after action a is performed;
- [a]P is true if P must be true after action a is performed.
Dynamic logic has been a very fruitful idea, used especially in concurrency, artificial intelligence and formal linguistics.