  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.
