Formal Methods for An Iterated Volunteer's Dilemma

TL;DR

This paper introduces a formal framework for analyzing the Volunteer's Dilemma using game theory, focusing on model correctness, strategy synthesis, and reward analysis in multi-agent interactions.

Contribution

It formulates the Volunteer's Dilemma as a stochastic multi-player game and develops methods for verification, strategy synthesis, and reward analysis, advancing formal analysis tools for such dilemmas.

Findings

Verified model correctness and reachability properties.

Constructed strategy synthesis graphs for optimal trajectories.

Analyzed parameter effects on rewards over finite horizons.

Abstract

Game theory provides a framework for studying communication dynamics and emergent phenomena arising from rational agent interactions. We present a model framework for the Volunteer's Dilemma with four key contributions: (1) formulating it as a stochastic concurrent nn n-player game, (2) developing properties to verify model correctness and reachability, (3) constructing strategy synthesis graphs to identify optimal game trajectories, and (4) analyzing parameter correlations with expected local and global rewards over finite time horizons.