Hinweis
Dieser Eintrag wurde automatisch aus einem Altsystem migriert. Die Daten wurden nicht überprüft und entsprechen eventuell nicht den Qualitätskriterien des vorliegenden Systems.
Ábrahám, E., Bartocci, E., Bonakdarpour, B., & Dobe, O. (2020). Probabilistic Hyperproperties with Nondeterminism. In Automated Technology for Verification and Analysis (pp. 518–534). https://doi.org/10.1007/978-3-030-59152-6_29
E191-01 - Forschungsbereich Cyber-Physical Systems
-
Erschienen in:
Automated Technology for Verification and Analysis
-
Datum (veröffentlicht):
2020
-
Veranstaltungsname:
Proc. of ATVA 2020: the 18th International Symposium on Automated Technology for Verification and Analysis
en
Veranstaltungszeitraum:
19-Okt-2020 - 23-Okt-2020
-
Veranstaltungsort:
Hanoi, Vietnam
-
Umfang:
17
-
Peer Reviewed:
Ja
-
Abstract:
We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic HyperPCTL, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification ov...
We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic HyperPCTL, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that HyperPCTL model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.
