Richard M. Karp Distinguished Lecture — Back to the Future: A Fresh Look at Linear Temporal Logic

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 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, and earned Vardi and Wolper the 2000 Gödel Prize. However, as a side-effect, 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 the work of Manna and Pnueli, 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.

If you require accommodation for communication, please contact our Access Coordinator at simonsevents [at] berkeley.edutarget="_blank" with as much advance notice as possible.