Automatic verification of competitive stochastic systems. (English) Zbl 1352.68150

Flanagan, Cormac (ed.) et al., Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28755-8/pbk). Lecture Notes in Computer Science 7214, 315-330 (2012).
Summary: 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.
For the entire collection see [Zbl 1238.68014].


68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
91A15 Stochastic games, stochastic differential games
91A80 Applications of game theory


Full Text: DOI