Introducing Asynchronicity to Probabilistic Hyperproperties

Autor:	Gerlach, Lina, Dobe, Oyendrila, Ábrahám, Erika, Bartocci, Ezio, Bonakdarpour, Borzoo
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science F.3.1
Druh dokumentu:	Working Paper
Popis:	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. Comment: to be published in the Proceedings of QEST 2023
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2307.05282 Zobrazit plný text záznamu View this record from Arxiv