In this talk, we will see an overview of classical results about temporal logics (LTL, CTL, CTL*,…):  basic definitions, examples of properties, expressiveness, classical techniques for their decision procedures, complexity… We will also present several extensions of these logics and their use in the verification area.

----

François Laroussinie is a  Professor at Univeristy Paris Diderot - Paris 7, Laboratory IRIF. His research activities concern the verification and specification of reactive, critical or embedded systems, focusing on: temporal logics for specifying reactive systems, model-checking complexity and verification of timed systems.

Web-page: https://www.irif.univ-paris-diderot.fr/~francoisl/