Probabilistic Strategy Logic with Degrees of Observability

TL;DR

This work introduces Opacity Probabilistic Strategy Logic ($oPSL$), an extension of Probabilistic Strategy Logic that explicitly handles information transparency and observability in partially observable stochastic multi-agent systems. It defines observability operators ${ m odot}_i$ and degree-of-observability terms ${f D}_{eta,i}(ullet)$ to express which behaviours are observable to which agents under strategy bindings, for both state properties and actions. The authors develop a model-checking framework that reduces $oPSL$ satisfaction to first-order real arithmetic via a translation into a finite set of formulas, using automata-based constructions (including Büchi, Rabin, Streett, and Safra determinization) and product Markov chains. They prove decidability under memoryless strategies and provide a detailed complexity analysis showing triple-exponential space in the formula and double-exponential dependence on the system size, reflecting the intricate automata-theoretic machinery. The framework enables formal reasoning about information leakage, privacy, and security in MAS, with potential applications in security, privacy, game theory, and AI safety, and suggests future work integrating epistemic reasoning and dynamic/multi-layered agent structures.

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.

Figures (1)

• Figure 1: Simple message interception scenario

Theorems & Definitions (10)

• definition 1
• definition 2
• definition 3
• definition 4
• definition 5
• definition 6
• definition 7
• theorem 1
• theorem 2
• proof : Proof sketch