There has been considerable work on reasoning about the strategic ability of agents under imperfect information. However, existing logics such as Probabilistic Strategy Logic are unable to express properties relating to information transparency. Information transparency concerns the extent to which agents' actions and behaviours are observable by other agents. Reasoning about information transparency is useful in many domains including security, privacy, and decision-making. In this paper, we present a formal framework for reasoning about information transparency properties in stochastic multi-agent systems. We extend Probabilistic Strategy Logic with new observability operators that capture the degree of observability of temporal properties by agents. We show that the model checking problem for the resulting logic is decidable.

翻译：在关于智能体在非完美信息下策略能力推理方面已有大量研究。然而，现有逻辑如概率策略逻辑无法表达与信息透明度相关的属性。信息透明度关注智能体的行动和行为被其他智能体观测的程度。对信息透明度的推理在安全、隐私和决策制定等多个领域具有重要价值。本文提出了一个用于随机多智能体系统中信息透明度属性推理的形式化框架。我们通过引入新的可观测性算子扩展了概率策略逻辑，这些算子能够捕捉智能体对时序属性的可观测程度。我们证明了所得逻辑的模型检测问题是可判定的。