Bi-Weekly Meeting: Carolina Gerlach

Mittwoch, 17.05.2023, 10.30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragende: Carolina Gerlach



Many interesting requirements, such as information-flow security policies, cannot be expressed as trace properties. Instead, security policies like noninterference are hyperproperties, which relate different executions of a system. Probabilistic hyperproperties express probabilistic relations between several independent executions of a system. Probabilistic hyperproperties can, for example, be expressed in HyperPCTL, which extends PCTL by quantification over states.

In this talk, I will give a gentle introduction to probabilistic hyperproperties, and present current work on an asynchronous extension of HyperPCTL, where the traces in different quantified computation trees do not have to evolve in lockstep anymore. This extension allows to capture the asynchronous nature of concurrent programs more accurately.