Formal Methods for An Iterated Volunteer's Dilemma

We propose an iterated version of Volunteer's Dilemma game through PRISM Model Checker (PRISM henceforth). This is useful because with this software, one can easily tune game parameters to get intuition of game dynamics. This can allow us to see what setting changes correlate with change in expected reward for each player. Additionally, PRISM can provide us a probabilistic graph that reflects a strategy that is optimal (or approximately optimal). Previous works [2] define public good game as a concurrent stochastic game, evaluating optimal strategies under a fixed set of parameters deciding the length of the game and the scaling factor associated with resource distribution.