Parameter Synthesis for Probabilistic Hyperproperties
A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. We, in particular, solve the following problem: given a probabilistic hyperproperty φ and a parametric discrete-time Markov chain M, whose transition probability matrix is specified in terms of a set of parameters, our goal is to compute an evaluation functions for each of these parameters, such that M satisfies φ. We solve this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We further work on finding range of values which would satisfy or not satisfy such equations. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.
Oyendrila Dobe is a second year PhD student in the Department of Computer Science at Iowa State University. She is reasearching on information flow security in the Dependable Systems Lab.