In the late 1970s, Amir Pnueli introduced Linear Temporal Logic (LTL) into computer science as a framework for specifying and formally verifying concurrent programs, a contribution that earned him the 1996 Turing Award. During the 1980s, in collaboration with Zohar Manna and others, he proceeded to classify the properties expressible in LTL, and to design proof rules for program verification. In particular, in joint work with Cheng and Manna, he proved an important Normalization Theorem for LTL.

In 1985 Vardi and Wolper showed that, by translating LTL formulas into automata on infinite words, automata-theoretic algorithms and technology can be used to solve verification problems more efficiently. This gave an enormous impulse to formal verification, but it also took logic techniques out of the limelight. By the early 1990s, a large part of the verification community had demoted LTL to a specification language, sort of syntax for automata.

In the last years, Jan Kretinsky, Salomon Sickert and myself have conducted a research program under the slogan ``the future needs LTL back''. We have shown that logic techniques, and in particular a new normalization algorithm, help to translate LTL into smaller and better automata for modern applications, like probabilistic verification and automatic program synthesis. The talk will present recent highlights of our work.