Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Expectation vs. Reality: Towards Verification of Psychological Games

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

TL;DR

Methods to solve Psychological games and implement them within PRISM-games, a formal verification tool for stochastic games are proposed, showing the usefulness of the approach on several case studies, including human behaviour in 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.

Expectation vs. Reality: Towards Verification of Psychological Games

TL;DR

Methods to solve Psychological games and implement them within PRISM-games, a formal verification tool for stochastic games are proposed, showing the usefulness of the approach on several case studies, including human behaviour in 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.

Paper Structure

This paper contains 9 sections, 1 theorem, 17 equations, 12 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Equilibria Computation for Psychological Games
  4. Psychological Concurrent Stochastic Games
  5. Case Studies and Experimental Results
  6. Reciprocity and Ultimatum Games
  7. Traffic Games
  8. Conclusions
  9. Appendix

Key Result

lemma 1

A pair $(b,\sigma)$ comprising a belief profile $b$ and a strategy profile $\sigma{=}(\sigma_1,\dots,\sigma_n)$ of ${\sf N_P} = (N,A,u)$ is a PE if and only if (pe1new-eqn) and the following conditions are satisfied: where $\eta_{a_i}$ is the pure strategy that picks action $a_i$ with probability 1.

Figures (12)

  • Figure 1: Player utilities (left) and total expected utility (right) for Example \ref{['examp:solve']}.
  • Figure 2: Reward structures for the ultimatum game, modelled in PRISM-games.
  • Figure 3: Reciprocity and ultimatum games in extensive form. The utilities for players 1 and 2 are given in the top and bottom rows of each leaf node, respectively.
  • Figure 4: Possible social welfare PEs for the reciprocity (top) and ultimatum (bottom) games for a range of reciprocity sensitivities $\theta_1,\theta_2$. We show the strategy (probabilities ${p_\mathit{g}}$, ${p_\mathit{a}}$ of choosing $\mathit{greedy}$, $\mathit{accept}$) and values (utilities $u_1$ and $u_2$).
  • Figure 5: An illustration for the pedestrian crossing scenario.
  • ...and 7 more figures

Theorems & Definitions (10)

  • definition 1: Normal form game
  • definition 2: Strategy and strategy profile
  • definition 3: Support
  • definition 4: Best response
  • definition 5: Nash equilibrium
  • definition 6: Social welfare NE
  • definition 7: Normal form psychological game
  • definition 8: Psychological Nash equilibrium
  • lemma 1
  • definition 9: Concurrent stochastic game