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.

提出一种新方法，利用量化的透明度分析技术来量化分析部分可观测多智能体系统的可观测性质，并通过量化分析技术以及模型验证技术实现了该方法。