Introducing Asynchronicity to Probabilistic Hyperproperties

arXiv (Cornell University)

Abstract

Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where quantification over probabilistic schedulers resolves potential non-determinism. In this paper we propose an extension named AHyperPCTL to additionally introduce asynchronicity between the observed executions by quantifying over stutter-schedulers, which may randomly decide to delay scheduler decisions by idling. To our knowledge, this is the first asynchronous extension of a probabilistic branching-time hyperlogic. We show that AHyperPCTL can express interesting information-flow security policies, and propose a model checking algorithm for a decidable fragment.

Authors 5

1. Lina Gerlach Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

   RWTH Aachen University, Aachen, Germany

2. Oyendrila Dobe

   Michigan State University

   Affiliation as printed

   Michigan State University, East Lansing, MI, USA

3. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

   RWTH Aachen University, Aachen, Germany

4. Ezio Bartocci

   TU Wien

   Affiliation as printed

   Technische Universität Wien, Vienna, Austria

5. Borzoo Bonakdarpour

   Michigan State University

   Affiliation as printed

   Michigan State University, East Lansing, MI, USA