# On Quantified Observability Analysis in Multiagent Systems

arXiv: https://arxiv.org/abs/2310.02614 · HTML: https://mlsanity.com/paper/2310.02614/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 33 references that are in the map.
- First posted on arXiv 4 Oct 2023.

## Builds on (most cited first, 4 of 4)

- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games](https://mlsanity.com/paper/1811.07145/) (2018)
- [On-the-fly Strategy Adaptation for ad-hoc Agent Coordination](https://mlsanity.com/paper/2203.08015/) (2022)
- [The Complexity of Monitoring Hyperproperties](https://mlsanity.com/paper/2101.07847/) (2021)

## Abstract (arXiv)

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.