modal logic

modal logic Any logical system that allows the use of modal operators designed to explore modes of truth. The two most common operators are “necessity” and “possibility”, usually written as □ and ◇, where □F expresses “F is necessarily true” and ◇F that “F is possibly true”. The objective of modal logic is to pin down meanings and laws of reasoning for these modes of truth. Modal logic has been developed in philosophy and is now the basis of advanced technologies in computer science.

For a modal operator α, the value of a formula αF in an interpretation I depends on the values of F in a whole class of interpretations related to I, rather than on the value of F in just I itself as is the case in a nonmodal logic. Thus □F is true in an interpretation (or world) w if F is true in all worlds w′ related to (or accessible from) w, while ◇F is true in w if F is true in at least one such w′. In discussing the semantics of modal logic, therefore, one considers frames of the form (W,R), where W is a set of worlds and R is an accessibility relation on W. Each world attaches a value to all the primitive symbols in the language.

In dynamic logic the modal operators correspond to programs, and the worlds correspond to states of execution. Then the formula αF is true in a particular state s if F is true in all states reachable from s by running the program α. Dynamic logic is similar to Hoare logic in the fact that its formulas involve both programming and logical constructs.

In temporal logics the modal operators deal with interpretations that might depend on the time: formulas express “F is sometimes true” or “F is always true”. Other modal operators express notions of belief, desirability, and obligation. All these ideas are of great relevance in reasoning about programs and systems. Hence recent years have seen extensive use of modal logics in program verification and formal specification, especially for concurrent programs and systems.