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.

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