  Probabilistic hyperproperties specify quantitative relations between the
probabilities of reaching different target sets of states from different
initial sets of states. This class of behavioral properties is suitable for
capturing important security, privacy, and system-level requirements. We
propose a new approach to solve the controller synthesis problem for Markov
decision processes (MDPs) and probabilistic hyperproperties. Our specification
language builds on top of the logic HyperPCTL and enhances it with structural
constraints over the synthesized controllers. Our approach starts from a family
of controllers represented symbolically and defined over the same copy of an
MDP. We then introduce an abstraction refinement strategy that can relate
multiple computation trees and that we employ to prune the search space
deductively. The experimental evaluation demonstrates that the proposed
approach considerably outperforms HyperProb, a state-of-the-art SMT-based model
checking tool for HyperPCTL. Moreover, our approach is the first one that is
able to effectively combine probabilistic hyperproperties with additional
intra-controller constraints (e.g. partial observability) as well as
inter-controller constraints (e.g. agreements on a common action).

Logic in Computer Science;Artificial Intelligence;Robotics