Linear Temporal Logic

Linear Temporal Logic (LTL) is a modal temporal logic in which time is treated as a discrete, linear sequence of states extending infinitely into the future. 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 algorithmically 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.

The restriction to a single linear timeline is not a limitation to be overcome but a disciplinary choice to be defended. Branching-time logics like CTL permit reasoning about alternative futures, but 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.