In multiagent systems (MASs), agents' observation upon system behaviours may improve the overall team performance, but may also leak sensitive information to an observer. A quantified observability analysis can thus be useful to assist decision-making in MASs by operators seeking to optimise the relationship between performance effectiveness and information exposure through observations in practice. This paper presents a novel approach to quantitatively analysing the observability properties in MASs. The concept of opacity is applied to formally express the characterisation of observability in MASs modelled as partially observable multiagent systems. We propose a temporal logic oPATL to reason about agents' observability with quantitative goals, which capture the probability of information transparency of system behaviours to an observer, and develop verification techniques for quantitatively analysing such properties. We implement the approach as an extension of the PRISM model checker, and illustrate its applicability via several examples.

翻译：在多智能体系统中，智能体对系统行为的观测可能提升整体团队性能，但也可能向观察者泄露敏感信息。因此，量化的可观测性分析有助于操作者通过实际观测来优化绩效与信息暴露之间的平衡，从而辅助多智能体系统决策。本文提出了一种量化分析多智能体系统可观测性属性的新方法。通过将不透明性概念应用于建模为部分可观测多智能体系统的可观测性表征，我们提出了时序逻辑oPATL用于推理智能体在量化目标下的可观测性——该逻辑可量化系统行为对观察者的信息透明概率，并开发了相应的验证技术以实现此类属性的量化分析。我们将该方法实现为PRISM模型检测器的扩展模块，并通过多个示例验证其适用性。