Automatic Verification of Competitive Stochastic Systems

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHEN Taolue FOREJT Vojtěch KWIATKOWSKA Marta PARKER David SIMAITIS Aistis

Year of publication 2013
Type Article in Periodical
Magazine / Source Formal Methods in System Design
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/s10703-013-0183-7
Field Informatics
Keywords Quantitative verification; Probabilistic model checking; Stochastic multi-player games; Probabilistic temporal logic
Description We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic 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 give an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of the PRISM tool. 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 in Microgrids and collective decision making for autonomous systems.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.