 | EasyChair Smart Slide | Docs/Log in |
Title:Parameter Synthesis for Probabilistic Hyperproperties Conference:LPAR23 Tags:differential privacy, discrete time markov chain, Information-Flow Security, model checking, parameter synthesis, parameter synthesis algorithm, parametric discrete time markov, parametric dtmc model, probabilistic conformance, probabilistic hyperproperty, Probabilistic Systems, randomized response, reachhyperpctl quantified formula, satisfying parameter configuration and Synthesis Abstract: In this paper, we study the parameter synthesis problem 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 discrete-time Markov chain with parametric transition probabilities, compute regions of parameter configurations that instantiate the Markov chain to satisfy the hyperproperty, and regions that lead to violation. 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 illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.  |
|     |
