Verification of Nash-Equilibrium for Probabilistic BAR Systems

A BAR system specifies a cooperation between agents who can be altruistic when they follow the specified behaviours, Byzantine when they randomly deviate from specifications and rational when they deviate to increase their own benefits. We consider whether a rational agent indeed follows the specification of a probabilistic BAR system as verifying whether the system is a Nash-equilibrium in the corresponding stochastic games. In this article, we propose an intuitive specification for probabilistic BAR systems and an algorithm to automatically verify Nash-equilibrium. To validate our implementation of the algorithm, we present two case studies - the three-player Rock-paper-scissors game and a probabilistic secret sharing protocol.