# Expectation vs. Reality: Towards Verification of Psychological Games

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

## Key facts

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

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

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Automatic Verification of Concurrent Stochastic Systems](https://mlsanity.com/paper/2008.04613/) (2020)
- [Correlated Equilibria and Fairness in Concurrent Stochastic Games](https://mlsanity.com/paper/2201.09702/) (2022)
- [Game Theoretic Analysis of Road User Safety Scenarios Involving Autonomous Vehicles](https://mlsanity.com/paper/1803.02393/) (2018)
- [Multi-player Equilibria Verification for Concurrent Stochastic Games](https://mlsanity.com/paper/2007.03365/) (2020)

## Abstract (arXiv)

Game theory provides an effective way to model strategic interactions among rational agents. In the context of formal verification, these ideas can be used to produce guarantees on the correctness of multi-agent systems, with a diverse range of applications from computer security to autonomous driving. Psychological games (PGs) were developed as a way to model and analyse agents with belief-dependent motivations, opening up the possibility to model how human emotions can influence behaviour. In PGs, players' utilities depend not only on what actually happens (which strategies players choose to adopt), but also on what the players had expected to happen (their belief as to the strategies that would be played). Despite receiving much attention in fields such as economics and psychology, very little consideration has been given to their applicability to problems in computer science, nor to practical algorithms and tool support. In this paper, we start to bridge that gap, proposing methods to solve PGs and implementing them within PRISM-games, a formal verification tool for stochastic games. We discuss how to model these games, highlight specific challenges for their analysis and illustrate the usefulness of our approach on several case studies, including human behaviour in traffic scenarios.