temporal logic

Ordinary logic talks about what is true, full stop. But when you reason about a running program or a protocol, truth changes over time: a lock is held now but released later, a request will eventually be answered, an error must never occur. Temporal logic is logic extended with operators that talk about time — about what holds now, next, always, and eventually — so you can write precise statements about how a system behaves as it runs.

It adds a handful of temporal operators on top of ordinary propositions. In the common linear-time flavour (LTL), reading along an infinite sequence of states, the key operators are: G p ('globally', p holds at every future moment — a safety claim like 'never crash'), F p ('finally' or eventually, p holds at some future moment — a liveness claim like 'eventually respond'), X p ('next', p holds at the very next step), and p U q ('until', p holds until q becomes true). These compose: G F p reads 'infinitely often p' (always, eventually, p again), the exact pattern Buchi automata accept; G (request implies F response) says 'every request is eventually answered'. Each formula describes a set of acceptable infinite behaviours.

Temporal logic is the specification language of formal verification. Engineers state desired properties of hardware and software — mutual exclusion, deadlock-freedom, eventual delivery — as temporal formulas, and a model checker then proves the system satisfies them or hands back a counterexample trace. The link that makes this automatic is precisely the connection to Buchi automata: an LTL formula can be compiled into a Buchi automaton accepting exactly the runs that satisfy it, turning a logical question into an automata question. There are different temporal logics (LTL is linear, CTL is branching, distinguishing 'on all futures' from 'on some future'), each with its own expressiveness and trade-offs.