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.

David Parker is a Lecturer in Computer Science at the University of Birmingham. Prior to that, he was a postdoctoral researcher at the University of Oxford. His main research interests are in the area of formal verification, with a particular focus on the analysis of quantitative aspects such as probabilistic and real-time behaviour. Recent work includes efficient techniques for scalable verification (e.g. abstraction, compositionality), game-theoretic verification methods, and applications of these approaches to areas such as systems biology, DNA computing and computer security. He leads development of the widely used probabilistic verification tool PRISM, regularly serves on the programme committees of international conferences such as CONCUR, QEST, CMSB and SAC, and frequently gives invited tutorials at summer-schools and workshops.