Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 1/2013

01-08-2013

Automatic verification of competitive stochastic systems

Authors: Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, Aistis Simaitis

Published in: Formal Methods in System Design | Issue 1/2013

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.
previous article Time-triggered runtime verification
next article Ranking function synthesis for bit-vector relations

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
Rational values can be handled by re-scaling all rewards by the lowest common multiple of the denominators of rewards appearing in the game. Note that re-scaling does not increase the size of the model, so the stated complexity results are not affected.
 
2
The tool is currently available from: http://​www.​prismmodelchecke​r.​org/​games/​.
 
Literature
1.
Aizatulin M, Schnoor H, Wilke T (2009) Computationally sound analysis of a probabilistic contract signing protocol. In: Proc of the 14th European symposium on research in computer security (ESORICS’09). LNCS, vol 5789. Springer, Berlin, pp 571–586
2.
3.
Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, MOCHA ST (1998) Modularity in model checking. In: Proc of the 10th international conference on computer aided verification (CAV’98), Vancouver. LNCS, vol 1427. Springer, Berlin, pp 521–525 CrossRef
4.
Andova S, Hermanns H, Katoen J-P (2003) Discrete-time rewards model-checked. In: Proc of the formal modeling and analysis of timed systems (FORMATS’03). LNCS, vol 2791. Springer, Berlin, pp 88–104 CrossRef
5.
Baier C, Brázdil T, Größer M, Kucera A (2007) Stochastic game logic. In: Proc of the 4th international conference on quantitative evaluation of systems (QEST’07). IEEE Press, New York, pp 227–236 CrossRef
6.
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge MATH
7.
Ballarini P, Fisher M, Wooldridge M (2006) Uncertain agent verification through probabilistic model-checking. In: Proc of the 3rd international workshop on safety and security in multi-agent systems (SASEMAS’06)
8.
Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proc of the 15th conference on foundations of software technology and theoretical computer science (FSTTCS’95). LNCS, vol 1026. Springer, Berlin, pp 499–513 CrossRef
9.
Brihaye T, Markey N, Ghannem M, Rieg L (2008) Good friends are hard to find! In: Demri S, Jensen C (eds) Proc of the 15th international symposium on temporal representation and reasoning (TIME’08). IEEE Press, New York, pp 32–40
10.
11.
Cerný P, Chatterjee K, Henzinger T, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S (eds) Proc of the 23rd international conference on computer aided verification (CAV’11). LNCS, vol 6806. Springer, Berlin, pp 243–259 CrossRef
12.
Chatterjee K (2007) Stochastic ω-regular games. PhD thesis, University of California at Berkeley
13.
Chatterjee K, Henzinger T (2008) Value iteration. In: 25 years of model checking, pp 107–138 CrossRef
14.
Chatterjee K, Henzinger T, Jobstmann B, Gist AR (2010) A solver for probabilistic games. In: Proc of the 22nd international conference on computer aided verification (CAV’10). LNCS. Springer, Berlin, pp 665–669 CrossRef
15.
Chatterjee K, Jurdzinski M, Henzinger T (2004) Quantitative stochastic parity games. In: Munro JI (ed) Proc of the 15th annual ACM-SIAM symposium on discrete algorithms (SODA’04). SIAM, Philadelphia, pp 121–130
16.
Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A (2012) Automatic verification of competitive stochastic systems. In: Flanagan C, König B (eds) Proc of the 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS’12). LNCS, vol 7214. Springer, Berlin, pp 315–330 CrossRef
17.
Chen T, Kwiatkowska M, Parker D, Simaitis A (2011) Verifying team formation protocols with probabilistic model checking. In: Proc of the 12th international workshop on computational logic in multi-agent systems (CLIMA XII 2011). LNCS, vol 6814. Springer, Berlin, pp 190–297 CrossRef
18.
Chen T, Lu J (2007) Probabilistic alternating-time temporal logic and model checking algorithm. In: Proc of the 4th international conference on fuzzy systems and knowledge discovery (FSKD’07). IEEE Press, New York, pp 35–39 CrossRef
19.
Condon A (1993) On algorithms for simple stochastic games. In: Advances in computational complexity theory. DIMACS series in discrete mathematics and theoretical computer science, vol 13, pp 51–73
20.
21.
de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proc of the 10th international conference on concurrency theory (CONCUR’99). LNCS, vol 1664. Springer, Berlin, pp 66–81 CrossRef
22.
de Alfaro L, Henzinger T (2000) Concurrent omega-regular games. In: Proc of the 15th annual IEEE symposium on logic in computer science. IEEE Comput Soc, Los Alamitos, pp 141–154
23.
Filar J, Vrieze K (1997) Competitive Markov decision processes. Springer, Berlin MATH
24.
Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems (SFM’11). LNCS, vol 6659. Springer, Berlin, pp 53–113 CrossRef
25.
Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535 MATHCrossRef
26.
Hildmann H, Saffre F (2011) Influence of variable supply and load flexibility on demand-side management. In: Proc of the 8th international conference on the European energy market (EEM’11), pp 63–68
27.
Kremer S, Raskin J-F (2003) A game-based verification of non-repudiation and fair exchange protocols. J Comput Secur 11(3):399–430
28.
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc of the 23rd international conference on computer aided verification (CAV’11). LNCS, vol 6806. Springer, Berlin, pp 585–591 CrossRef
29.
Laroussinie F, Markey N, Oreiby G (2007) On the expressiveness and complexity of ATL. In: Seidl H (ed) Proc of the 10th international conference on foundations of software science and computational structures (FOSSACS’07). LNCS, vol 4423. Springer, Berlin, pp 243–257
30.
Lomuscio A, Qu H, Raimondi F (2009) MCMAS: a model checker for the verification of multi-agent systems. In: Proc of the 21st international conference on computer aided verification (CAV’09). LNCS, vol 5643. Springer, Berlin, pp 682–688 CrossRef
31.
32.
33.
34.
Schnoor H (2010) Strategic planning for probabilistic games with incomplete information. In: Proc of the 9th international conference on autonomous agents and multiagent systems (AAMAS’10), pp 1057–1064
35.
Ummels M (2010) Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen University
36.
van der Hoek W, Wooldridge M (2003) Model checking cooperation, knowledge, and time—a case study. Res Econ 57(3):235–265 CrossRef
37.
Zhang C, Pang J (2010) On probabilistic alternating simulations. In: Calude C, Sassone V (eds) Proc of the 6th IFIP conference on theoretical computer science (TCS’10). IFIP, vol 323. Springer, Berlin, pp 71–85 CrossRef
38.
Zhang C, Pang J (2012) An algorithm for probabilistic alternating simulation. In: Bieliková M, Friedrich G, Gottlob G, Katzenbeisser S, Turán G (eds) Proc of the 38th conference on current trends in theory and practice of computer science (SOFSEM’12). LNCS, vol 7147. Springer, Berlin, pp 431–442
Metadata
Title
Automatic verification of competitive stochastic systems
Authors
Taolue Chen
Vojtěch Forejt
Marta Kwiatkowska
David Parker
Aistis Simaitis
Publication date
01-08-2013
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 1/2013
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-013-0183-7

Premium Partner

    Image Credits