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).

翻译：概率超属性规定了从不同初始状态集到达不同目标状态集的概率之间的定量关系。该类行为属性适用于描述重要的安全性、隐私性和系统级需求。我们提出了一种新方法来解决马尔可夫决策过程（MDP）与概率超属性的控制器合成问题。我们的规约语言基于HyperPCTL逻辑构建，并通过在合成控制器上施加结构约束对其进行增强。该方法始于一个符号化表示且定义在同一MDP副本上的控制器族。随后，我们引入了一种抽象精化策略，该策略可关联多个计算树，并用于演绎地剪枝搜索空间。实验评估表明，所提方法显著优于HyperProb（一种用于HyperPCTL的先进基于SMT的模型检测工具）。此外，我们的方法是首个能够有效将概率超属性与控制器内约束（如部分可观测性）以及控制器间约束（如对共同行动的协议）相结合的方法。