<div class="csl-bib-body">
<div class="csl-entry">Dobe, O., Ábrahám, E., Bartocci, E., & Bonakdarpour, B. (2022). Model checking hyperproperties for Markov decision processes. <i>Information and Computation</i>, <i>289</i>(Part B), Article 104978. https://doi.org/10.1016/j.ic.2022.104978</div>
</div>
-
dc.identifier.issn
0890-5401
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/142176
-
dc.description.abstract
We study the problem of formalizing and checking probabilistic hyperproperties for Markov decision processes (MDPs). We introduce the temporal logic HyperPCTL that allows explicit and simultaneous quantification over schedulers as well as probabilistic computation trees. We show that the logic can express important quantitative requirements in security and privacy such as probabilistic noninterference, differential privacy, timing side-channel countermeasures, and probabilistic conformance testing. We show that HyperPCTL model checking over MDPs is in general undecidable, but restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language. Finally, we demonstrate the applicability of our method by providing experimental results for verification, and we show how it can be used to solve even certain synthesis problems.
en
dc.language.iso
en
-
dc.publisher
ACADEMIC PRESS INC ELSEVIER SCIENCE
-
dc.relation.ispartof
Information and Computation
-
dc.subject
Hyperproperties
en
dc.subject
Information leakage
en
dc.subject
Markov models
en
dc.subject
Model checking
en
dc.subject
Policy synthesis
en
dc.title
Model checking hyperproperties for Markov decision processes