Automatic Verification of Competitive Stochastic Systems
Abstract:
Many situations, for example smart grid systems, call for models and analysis methods which exhibit stochasticity and allow for the modelling of cooperative agent behaviour under possibly hostile environments. We adopt multi-player stochastic games as a modelling framework and develop techniques for reasoning about the collective ability of a set of players to achieve a goal. The properties that can be established in our framework include "can a group of agents collaborate so that the maximum expected energy cost of a collection of tasks is no greater than a given value, no matter what the other agents do?", which are expressible in a probabilistic and reward extension of the well-known alternating temporal logic ATL. We formulate a model checking algorithm for verifying properties expressed in this logic and implement the techniques in an extension of the probabilistic model checker PRISM (prismmodelchecker.org) called PRISM-games. We demonstrate the applicability and efficiency of our methods by deploying them to analyse and detect potential weaknesses in a variety of large case studies, including algorithms for energy management and collective decision making for autonomous systems.