Talk "Temporal Logics for Hyperproperties"

by Cesar Sanchez

Fri, 13 February 2026 at 09:27 am in Torino, Italy

Joint work with: Many co-authors

Abstract: Hyperproperties are properties of systems that require to reason simultaneous about multiple traces of the system under analysis. Examples include security policies such as noninterference, non-inference, observational determinism, declassification, etc and other properties like symmetry of schedulers and correctness of coding/decoding systems. However, most of these properties are typically expressed in an ad-hoc manner, instead of using an expressive logic or formal language and the corresponding reasonging systems. Standard temporal logics, like LTL, CTL and CTL* can only refer to a single path at a time and cannot express many hyperproperties of interest. In this talk, I will present HyperLTL and HyperCTL* that extend LTL and CTL* with quantification over multiple paths. I will discuss aspects of these logics, like model-checking, satisfiability and runtime verification, and recent extensions and possibilities for future research.