Parameter Synthesis for Probabilistic Hyperproperties

EPiC series in computing, vol. 73, pp. 12–

Abstract

In this paper, we study the parameter synthesis problem for probabilistic hyperproper- ties. A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. In particular, we solve the following problem: given a probabilistic hyperprop- erty ψ and discrete-time Markov chain D with parametric transition probabilities, compute regions of parameter configurations that instantiate D to satisfy ψ, and regions that lead to violation. We address this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.

Authors 4

1. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

   RWTH Aachen University, Aachen, Germany

2. Ezio Bartocci

   TU Wien

   Affiliation as printed

   TU Wien , Vienna , Austria

   TU Wien, Vienna, Austria

3. Borzoo Bonakdarpour

   Michigan State University

   Affiliation as printed

   Michigan State University , East Lansing , MI , USA

   Michigan State University, East Lansing, MI, USA

4. Oyendrila Dobe

   Iowa State University

   Affiliation as printed

   Iowa State University , Ames , IA , USA

   Iowa State University, Ames, IA, USA