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.

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