Expectation vs. Reality: Towards Verification of Psychological Games

TL;DR

This paper introduces methods to verify psychological games within formal verification frameworks, enabling analysis of belief-dependent motivations and human behavior in multi-agent systems like traffic scenarios.

Contribution

It proposes the first practical algorithms for solving psychological games and integrates them into PRISM-games, bridging a gap between game theory and computer science verification.

Findings

Developed methods to model and analyze psychological games.

Implemented algorithms within PRISM-games for practical verification.

Validated approach with case studies including traffic scenarios.

Abstract

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.