Automated Game-theoretic Verification for Probabilistic Systems

We present automatic verification techniques for stochastic multi-player games, which model probabilistic systems containing components that can either collaborate or compete in order to achieve particular goals. We give model checking algorithms for a temporal logic called rPATL, which allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We implement our techniques in an extension of the PRISM model checker and use them to analyse and detect potential weaknesses in systems such as algorithms for energy management and collective decision making for autonomous systems.

This is joint work with Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska and Aistis Simaitis.