We study the complexity of the problem of verifying differential privacy for while-like programs working over boolean values and making probabilistic choices. Programs in this class can be interpreted into finite-state discrete-time Markov Chains (DTMC). We show that the problem of deciding whether a program is differentially private for specific values of the privacy parameters is PSPACE-complete. To show that this problem is in PSPACE, we adapt classical results about computing hitting probabilities for DTMC. To show PSPACE-hardness we use a reduction from the problem of checking whether a program almost surely terminates or not. We also show that the problem of approximating the privacy parameters that a program provides is PSPACE-hard. Moreover, we investigate the complexity of similar problems also for several relaxations of differential privacy: R\'enyi differential privacy, concentrated differential privacy, and truncated concentrated differential privacy. For these notions, we consider gap-versions of the problem of deciding whether a program is private or not and we show that all of them are PSPACE-complete.

翻译：我们研究了针对基于布尔值进行概率选择的类while程序验证差分隐私问题的复杂性。该类程序可被解释为有限状态离散时间马尔可夫链（DTMC）。我们证明了对于特定隐私参数值，判断程序是否满足差分隐私的问题是PSPACE完全的。为证明该问题属于PSPACE，我们改进了关于计算DTMC命中概率的经典结论；为证明PSPACE困难性，我们使用了从判断程序是否几乎必然终止的问题到该问题的归约。我们还证明了近似程序提供的隐私参数的问题是PSPACE困难的。此外，我们研究了差分隐私的若干松弛变体（Rényi差分隐私、集中差分隐私和截断集中差分隐私）中类似问题的复杂性。对于这些概念，我们考虑判断程序是否满足隐私性的间隙版本问题，并证明所有这些问题均为PSPACE完全的。