Logic for Computer Science/Temporal Logic

Modal Logic

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

$◊P\leftrightarrow \mathrm{\neg }◻\mathrm{\neg }P.$