BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:a5713664-991e-42b1-8798-93bf1eae3fa0
X-WR-CALNAME:[M2F] Jean-Marc Talbot
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:a5713664-991e-42b1-8798-93bf1eae3fa0
DTSTAMP:20260919T174326Z
CLASS:PUBLIC
DESCRIPTION:** Reasoning about Quality in Hyperproperties **\n\nSecurity pr
 operties such as non-interference cannot be expressed as properties of ind
 ividual traces of a system. Therefore\, the notion of hyperproperties has 
 been introduced to overcome this limitation: a hyperproperty can express p
 roperties about pairs or more generally\, sets of traces. An extension of 
 the LTL logic (hyperLTL) has been proposed to define hyperproperties and s
 ome positive results such as decidability for the model-checking problem h
 ave been proven.\n\nMotivated by verifying quantitative security propertie
 s\, we propose extensions of HyperLTL following the proposal of similar ex
 tensions of LTL by Almagor et al.\, namely LTL[F] for quantitative operato
 rs and LTL[D] for discounting temporal operators. Such extensions aim to q
 uantify on how much a formula is satisfied by a system. We will present so
 me algorithms for model-checking those logics.
DTSTART;TZID=Europe/Paris:20240328T130000
DTEND;TZID=Europe/Paris:20240328T140000
LOCATION:Salle 178
SEQUENCE:0
SUMMARY:[M2F] Jean-Marc Talbot
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR