Introducing Asynchronicity to Probabilistic Hyperproperties
Autor: | Gerlach, Lina, Dobe, Oyendrila, Ábrahám, Erika, Bartocci, Ezio, Bonakdarpour, Borzoo |
---|---|
Rok vydání: | 2023 |
Předmět: | |
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: |