temporallogic

Temporal logic is a formalism for reasoning about propositions with respect to time. It is used to describe how truth values of statements evolve along sequences of states or across branching futures. The field distinguishes linear time temporal logic (LTL), which reasons along a single timeline, from branching time temporal logics such as Computation Tree Logic (CTL), which allow quantification over multiple possible futures. A more expressive framework, CTL*, subsumes both LTL and CTL.

Syntax and semantics: In LTL, the main operators are X (next), F (eventually), G (globally), and U (until). CTL uses path quantifiers A (for all paths) and E (exists a path) in combination with temporal operators. Formulas are interpreted over models called Kripke structures or labeled transition systems, consisting of states, a transition relation, and a labeling of states with propositions. The truth of an LTL formula is defined along a path, while CTL formulas are evaluated at states with the appropriate path quantifier.

Applications: Temporal logic underpins automatic verification and model checking, allowing designers to verify that a system satisfies safety properties (something bad never happens) and liveness properties (something good eventually happens). It is widely used in hardware and software verification, concurrent and distributed systems, protocol design, and controller synthesis. In artificial intelligence, temporal logic supports planning and reasoning about sequences of actions and events.

History and variants: Temporal logic developed from work in philosophy and formal semantics and was introduced to computer science by Amir Pnueli in 1977 to reason about concurrent programs. Branching-time logics were developed in the 1980s, with practical model-checking techniques that popularized LTL and CTL in industry. Real-time extensions such as Metric Temporal Logic (MTL) add quantitative timing constraints.

See also: modal logic, model checking, real-time systems.