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 $\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.$