Formal Methods for an Iterated Volunteer's Dilemma

Abstract

Game theory provides a paradigm through which we can study the evolving communication and phenomena that occur via rational agent interaction [10]. The Volunteer’s dilemma is a vastly studied game throughout literature that models agents as cooperative, rather than selfish, entities. In this work, we design a model framework and explore the Volunteer’s dilemma with the goals of 1) modeling it as a stochastic concurrent n-player game, 2) constructing properties to verify model correctness and reachability, 3) constructing strategy synthesis graphs to understand how the game is iteratively stepped through most optimally and, 4) analyzing a series of parameters to understand correlations with expected local and global rewards over a finite time horizon.