Automatic verification of competitive stochastic systems

作者：Chen Taolue; Forejt Vojtech; Kwiatkowska Marta; Parker David; Simaitis Aistis^*

来源：Formal Methods in System Design, 2013, 43(1): 61-92.

DOI：10.1007/s10703-013-0183-7

• Quantitative verification
• Probabilistic model checking
• Stochastic multi-player games
• Probabilistic temporal logic

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.

• 出版日期2013-8