On Quantified Observability Analysis in Multiagent Systems

TL;DR

This paper introduces a novel quantitative approach to analyze observability in multiagent systems, balancing performance and information exposure, using a new temporal logic and verification techniques implemented in PRISM.

Contribution

It presents a formal framework using opacity and a new temporal logic oPATL for quantitative observability analysis in MASs, with implementation in PRISM.

Findings

Effective formalization of observability using opacity.

Development of the oPATL logic for quantitative reasoning.

Implementation and demonstration of the approach on example systems.

Abstract

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.