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.

BibTeX Citation

@misc{gerlach2023introducing,
      title={Introducing Asynchronicity to Probabilistic Hyperproperties}, 
      author={Lina Gerlach and Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour},
      year={2023},
      eprint={2307.05282},
      archivePrefix={arXiv},
      primaryClass={cs.LO}
}