Probabilistic Strategy Logic with Degrees of Observability

TL;DR

This paper introduces an extension to Probabilistic Strategy Logic that incorporates degrees of observability, enabling reasoning about information transparency in stochastic multi-agent systems, with a proven decidable model checking process.

Contribution

It extends Probabilistic Strategy Logic with observability operators to formalize information transparency, a novel aspect not previously addressed.

Findings

Model checking for the extended logic is decidable.

The framework captures degrees of observability in multi-agent systems.

Enhances reasoning about security, privacy, and decision-making.

Abstract

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.