University of Oxford Logo University of OxfordDepartment of Computer Science - Home

The Rise and Fall of Linear Temporal Logic

Moshe Vardi (Rice University)



8th March 2012 (week 8, Hilary Term 2012)




Lecture Theatre B


One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the cannonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL).

Further info

Related series