# Probabilistic Strategy Logic with Degrees of Observability

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 26 references that are in the map.
- First posted on arXiv 19 Dec 2024.

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

- [Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games](https://mlsanity.com/paper/1811.07145/) (2018)
- [AutoHyper: Explicit-State Model Checking for HyperLTL](https://mlsanity.com/paper/2301.11229/) (2023)
- [Strategy Logic with Imperfect Information](https://mlsanity.com/paper/1805.12592/) (2018)
- [Algorithms in Real Algebraic Geometry: A Survey](https://mlsanity.com/paper/1409.1534/) (2014)
- [Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information](https://mlsanity.com/paper/2112.13621/) (2021)

## Abstract (arXiv)

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.