13:00
14:00

[M2F] Jean-Marc Talbot

** Reasoning about Quality in Hyperproperties **

Security properties such as non-interference cannot be expressed as properties of individual traces of a system. Therefore, the notion of hyperproperties has been introduced to overcome this limitation: a hyperproperty can express properties about pairs or more generally, sets of traces. An extension of the LTL logic (hyperLTL) has been proposed to define hyperproperties and some positive results such as decidability for the model-checking problem have been proven.

Motivated by verifying quantitative security properties, we propose extensions of HyperLTL following the proposal of similar extensions of LTL by Almagor et al., namely LTL[F] for quantitative operators and LTL[D] for discounting temporal operators. Such extensions aim to quantify on how much a formula is satisfied by a system. We will present some algorithms for model-checking those logics.

Salle 178