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

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 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.


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


Full Text: DOI Link


[1] Aizatulin, M; Schnoor, H; Wilke, T, Computationally sound analysis of a probabilistic contract signing protocol, No. 5789, 571-586, (2009), Berlin
[2] Alur, R; Henzinger, T; Kupferman, O, Alternating-time temporal logic, J ACM, 49, 672-713, (2002) · Zbl 1326.68181
[3] Alur, R; Henzinger, T; Mang, F; Qadeer, S; Rajamani, S; MOCHA, ST, Modularity in model checking, Vancouver, Berlin
[4] Andova, S; Hermanns, H; Katoen, J-P, Discrete-time rewards model-checked, No. 2791, 88-104, (2003), Berlin · Zbl 1099.68652
[5] Baier, C; Brázdil, T; Größer, M; Kucera, A, Stochastic game logic, 227-236, (2007), New York
[6] Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge · Zbl 1179.68076
[7] Ballarini, P; Fisher, M; Wooldridge, M, Uncertain agent verification through probabilistic model-checking, (2006) · Zbl 1273.68220
[8] Bianco, A; Alfaro, L; Thiagarajan, P (ed.), Model checking of probabilistic and nondeterministic systems, No. 1026, 499-513, (1995), Berlin · Zbl 1354.68167
[9] Brihaye, T; Markey, N; Ghannem, M; Rieg, L; Demri, S (ed.); Jensen, C (ed.), Good friends are hard to find!, 32-40, (2008), New York
[10] Bulling, N; Jamroga, W, What agents can probably enforce, Fundam Inform, 93, 81-96, (2009) · Zbl 1191.68648
[11] Cerný, P; Chatterjee, K; Henzinger, T; Radhakrishna, A; Singh, R; Gopalakrishnan, G (ed.); Qadeer, S (ed.), Quantitative synthesis for concurrent programs, No. 6806, 243-259, (2011), Berlin
[12] Chatterjee K (2007) Stochastic \(ω\)-regular games. PhD thesis, University of California at Berkeley · Zbl 1348.68255
[13] Chatterjee, K; Henzinger, T, Value iteration, 107-138, (2008) · Zbl 1143.68042
[14] Chatterjee, K; Henzinger, T; Jobstmann, B; Gist, AR, A solver for probabilistic games, 665-669, (2010), Berlin
[15] Chatterjee, K; Jurdzinski, M; Henzinger, T; Munro, JI (ed.), Quantitative stochastic parity games, 121-130, (2004), Philadelphia · Zbl 1318.91027
[16] Chen, T; Forejt, V; Kwiatkowska, M; Parker, D; Simaitis, A; Flanagan, C (ed.); König, B (ed.), Automatic verification of competitive stochastic systems, No. 7214, 315-330, (2012), Berlin · Zbl 1352.68150
[17] Chen, T; Kwiatkowska, M; Parker, D; Simaitis, A, Verifying team formation protocols with probabilistic model checking, No. 6814, 190-297, (2011), Berlin · Zbl 1348.68255
[18] Chen, T; Lu, J, Probabilistic alternating-time temporal logic and model checking algorithm, 35-39, (2007), New York
[19] Condon, A, On algorithms for simple stochastic games, No. 13, 51-73, (1993) · Zbl 0808.90141
[20] Courcoubetis, C; Yannakakis, M, The complexity of probabilistic verification, J ACM, 42, 857-907, (1995) · Zbl 0885.68109
[21] Alfaro, L; Baeten, J (ed.); Mauw, S (ed.), Computing minimum and maximum reachability times in probabilistic systems, No. 1664, 66-81, (1999), Berlin · Zbl 0949.93082
[22] Alfaro, L; Henzinger, T, Concurrent omega-regular games, 141-154, (2000), Los Alamitos
[23] Filar J, Vrieze K (1997) Competitive Markov decision processes. Springer, Berlin · Zbl 0934.91002
[24] Forejt, V; Kwiatkowska, M; Norman, G; Parker, D; Bernardo, M (ed.); Issarny, V (ed.), Automated verification techniques for probabilistic systems, No. 6659, 53-113, (2011), Berlin
[25] Hansson, H; Jonsson, B, A logic for reasoning about time and reliability, Form Asp Comput, 6, 512-535, (1994) · Zbl 0820.68113
[26] Hildmann, H; Saffre, F, Influence of variable supply and load flexibility on demand-side management, 63-68, (2011)
[27] Kremer, S; Raskin, J-F, A game-based verification of non-repudiation and fair exchange protocols, J Comput Secur, 11, 399-430, (2003)
[28] Kwiatkowska, M; Norman, G; Parker, D; Gopalakrishnan, G (ed.); Qadeer, S (ed.), PRISM 4.0: verification of probabilistic real-time systems, No. 6806, 585-591, (2011), Berlin
[29] Laroussinie, F; Markey, N; Oreiby, G; Seidl, H (ed.), On the expressiveness and complexity of ATL, No. 4423, 243-257, (2007), Berlin · Zbl 1142.68438
[30] Lomuscio, A; Qu, H; Raimondi, F, MCMAS: a model checker for the verification of multi-agent systems, No. 5643, 682-688, (2009), Berlin
[31] Martin, D, The determinacy of blackwell games, J Symb Log, 63, 1565-1581, (1998) · Zbl 0926.03071
[32] McIver A, Morgan C (2007) Results on the quantitative mu-calculus qMu. ACM Trans Comput Log 8(1). doi:10.1145/1182613.1182616 · Zbl 1367.68199
[33] Saffre F, Simaitis A (2012) Host selection through collective decision. ACM Trans Auton Adapt Syst 7(1). doi:10.1145/2168260.2168264
[34] Schnoor, H, Strategic planning for probabilistic games with incomplete information, 1057-1064, (2010)
[35] Ummels M (2010) Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen University
[36] Hoek, W; Wooldridge, M, Model checking cooperation, knowledge, and time—a case study, Res Econ, 57, 235-265, (2003)
[37] Zhang, C; Pang, J; Calude, C (ed.); Sassone, V (ed.), On probabilistic alternating simulations, No. 323, 71-85, (2010), Berlin · Zbl 1202.68464
[38] Zhang, C; Pang, J; Bieliková, M (ed.); Friedrich, G (ed.); Gottlob, G (ed.); Katzenbeisser, S (ed.); Turán, G (ed.), An algorithm for probabilistic alternating simulation, No. 7147, 431-442, (2012), Berlin · Zbl 1302.68205
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.