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.
"modal logic." A Dictionary of Computing. . Encyclopedia.com. (August 15, 2018). http://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/modal-logic
"modal logic." A Dictionary of Computing. . Retrieved August 15, 2018 from Encyclopedia.com: http://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/modal-logic