Skip to main content

Introducing Asynchronicity to Probabilistic Hyperproperties

Publication Type
Year of Publication
Conference/Journal Name
The International Conference on Quantitative Evaluation of SysTems (QEST)
Page Numbers
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.