Linear Temporal Logics beyond LTL

10^th January 2019, 13:30
Martin Zimmermann

Abstract

Linear Temporal Logic (LTL) is the most popular specification language for linear-time properties of reactive systems and LTL model checking is nowadays routinely applied in industrial settings. However, LTL suffers from several drawbacks, e.g., its inability to express timing constraints and is limited expressiveness.

In this introductory talk, I will present an overview of my work on generalisations of LTL overcoming these drawbacks. This includes parameterised logics which are able to express timing constraints, logics with the expressive power of the omega-regular and omega-context-free languages, and logics for expressing hyperproperties, which play an important role in security and privacy.