Logic for Computer Science/Temporal Logic

From Wikibooks, open books for an open world
< Logic for Computer Science
Jump to: navigation, search

Modal Logic[edit]

Modal logic expands propositional logic by operators for the modalities possibility and necessity. These basic modal operators are usually written \Box (or L) for necessarily and \Diamond (or M) for possibly. Each can be defined from the other in the following way:

\Diamond P \leftrightarrow \lnot\, \Box\, \lnot\, P.