Automatic Verification of Competitive Stochastic Systems

Warning

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

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

Year of publication 2012
Type Article in Proceedings
Conference Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.prismmodelchecker.org/papers/tacas12.pdf
Doi http://dx.doi.org/10.1007/978-3-642-28756-5_22
Field Informatics
Keywords stochastic games; branching time logics; multi-agent systems
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 a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on 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 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.