BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Future Lab Aachen - ECPv6.16.2//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Future Lab Aachen
X-ORIGINAL-URL:https://futurelab-aachen.de
X-WR-CALDESC:Veranstaltungen für Future Lab Aachen
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Berlin
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20200329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20201025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20210328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20211031T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20220327T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20221030T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Berlin:20210415T163000
DTEND;TZID=Europe/Berlin:20210415T180000
DTSTAMP:20260624T122411
CREATED:20210317T094557Z
LAST-MODIFIED:20210317T094557Z
UID:21548-1618504200-1618509600@futurelab-aachen.de
SUMMARY:Probabilistic Hyperproperties
DESCRIPTION:Erika Ábrahám: Probabilistic Hyperproperties \nFour decades ago\, Lamport used the notion of trace properties as a means to specify the correctness of individual executions of concurrent programs. This notion was later formalized and classified by Alpern and Schneider to safety and liveness properties. Temporal logics like LTL and CTL were built based on these efforts to give formal syntax and semantics to requirements of trace properties. Subsequently\, verification algorithms were developed to reason about individual executions of a system. \nHowever\, it turns out that many interesting requirements are not trace properties. For example\, important information-flow security policies (e.g. noninterference\, observational determinism) or service level agreements (e.g. mean response time\, percentage uptime) cannot be expressed as properties of individual execution traces of a system. Rather\, they are properties of sets of execution traces\, also known as hyperproperties. Temporal logics such as HyperLTL and HyperCTL∗ have been proposed to provide a unifying framework to express and reason about hyperproperties.\nThis talk is devoted to special class of hyperproperties: we ask the question what are hyperproperties in the context of systems with random behavior. We will discuss what are relevant probabilistic relations between independent executions of a system\, how we can formally express them in a temporal logic\, and how we can decide the truth of such statements. \n 
URL:https://futurelab-aachen.de/event/probabilistic-hyperproperties/
LOCATION:Audimax\, RWTH Aachen\, Wüllnerstrasse 9\, Aachen\, 52062\, Deutschland
CATEGORIES:Vortrag
END:VEVENT
END:VCALENDAR