Temporal logic is a form of modal logic in which the modal operators are used to denote the truth of a statement in the future or past. Application areas include linguistics and computer science, in particular program verification.