Statistical Model Checking for Probabilistic Hyperproperties

02/11/2019
by   Yu Wang, et al.
0

In this paper, we propose the temporal logic HyperPCTL^* that extends PCTL^* and HyperPCTL to reason about probabilistic hyperproperties. It allows expressing probabilistic hyperproperties with nested temporal and probability operators. We show that HyperPCTL can express important probabilistic information-flow security policies. Furthermore, for the first time, we investigate statistical model checking (SMC) algorithms for HyperPCTL^* specifications in discrete-time Markov chains (DTMC). To this end, we first study SMC for HyperPCTL^* specifications with non-nested probability operators for a desired confidence or significance level. Unlike existing SMC algorithms which are based on sequential probability ratio tests (SPRT), we use the Clopper-Pearson confidence interval to avoid the need of a priori knowledge on the indifference margin. Then, we extend the proposed SMC algorithms to HyperPCTL^* specifications with multiple probability operators that are nested in different ways. Finally, we evaluate the proposed algorithms on two examples, dining cryptographers and probabilistic causation.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset