LTL

LTL (Linear Temporal Logic) is a temporal logic that treats time as a single, discrete, infinite sequence of states. Its operators — G (globally), F (finally), X (next), and U (until) — quantify over this single timeline, making LTL the natural language for specifying sequential behavior in reactive and concurrent systems. Every LTL formula can be translated into a Büchi automaton, which is the foundational translation enabling model checking for liveness and safety properties.

LTL's satisfiability problem is PSPACE-complete, placing it at the precise boundary between tractable specification and computational intractability. It is incomparable in expressiveness with CTL: LTL captures fairness and certain sequencing properties that CTL cannot express, while CTL captures existential path properties beyond LTL's reach. The practical response is CTL*, which unifies both at greater algorithmic cost. See Linear Temporal Logic for a detailed exposition of the logic's semantics, algorithms, and applications.

The restriction of LTL to a single linear timeline is not a limitation to be overcome but a disciplinary choice to be defended. Most real verification problems concern what a system must do along the one future it actually executes — not what it might do along futures it does not take. The dominance of LTL in industrial verification reflects this: engineers verify sequences, not trees. The philosophical debate between linear and branching time is not settled in philosophy, but it has been settled in engineering — and linear time won.