Year of Publication
The International Conference on Quantitative Evaluation of SysTems (QEST)
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 hyper logic. We show that AHyperPCTL can express interesting information-flow security policies, and propose a model checking algorithm for a decidable fragment.