Temporal logic

Temporal logic is a branch of formal logic concerned with reasoning about propositions qualified in terms of time — whether something is true now, will eventually be true, or has always been true. Unlike classical logic, where propositions have fixed truth values, temporal logic introduces modal operators such as eventually (◇), always (□), and until (U) that make explicit the temporal structure of the systems being described. These logics are the specification language of model checking, where properties like 'the elevator will eventually reach the requested floor' or 'the system never enters an unsafe state' are expressed as temporal logic formulas and verified algorithmically against finite-state system models. The most widely used variants include Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and the more expressive CTL*, each offering different trade-offs between expressiveness and verification complexity.

Temporal logic reveals that the difference between a bug and a feature is often just a matter of timing — and that timing, unlike intention, can be formally checked.