{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T13:01:21Z","timestamp":1790427681511,"version":"4.1.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,2,16]],"date-time":"2013-02-16T00:00:00Z","timestamp":1360972800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10703-013-0183-7","type":"journal-article","created":{"date-parts":[[2013,2,15]],"date-time":"2013-02-15T09:07:53Z","timestamp":1360919273000},"page":"61-92","source":"Crossref","is-referenced-by-count":96,"title":["Automatic verification of competitive stochastic systems"],"prefix":"10.1007","volume":"43","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aistis","family":"Simaitis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,2,16]]},"reference":[{"key":"183_CR1","series-title":"LNCS","first-page":"571","volume-title":"Proc of the 14th European symposium on research in computer security (ESORICS\u201909)","author":"M Aizatulin","year":"2009","unstructured":"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\u201909). LNCS, vol 5789. Springer, Berlin, pp 571\u2013586"},{"issue":"5","key":"183_CR2","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur R, Henzinger T, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672\u2013713","journal-title":"J ACM"},{"key":"183_CR3","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Proc of the 10th international conference on computer aided verification (CAV\u201998)","author":"R Alur","year":"1998","unstructured":"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\u201998), Vancouver. LNCS, vol 1427. Springer, Berlin, pp 521\u2013525"},{"key":"183_CR4","series-title":"LNCS","first-page":"88","volume-title":"Proc of the formal modeling and analysis of timed systems (FORMATS\u201903)","author":"S Andova","year":"2003","unstructured":"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\u201903). LNCS, vol 2791. Springer, Berlin, pp 88\u2013104"},{"key":"183_CR5","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1109\/QEST.2007.38","volume-title":"Proc of the 4th international conference on quantitative evaluation of systems (QEST\u201907)","author":"C Baier","year":"2007","unstructured":"Baier C, Br\u00e1zdil T, Gr\u00f6\u00dfer M, Kucera A (2007) Stochastic game logic. In: Proc of the 4th international conference on quantitative evaluation of systems (QEST\u201907). IEEE Press, New York, pp 227\u2013236"},{"key":"183_CR6","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"183_CR7","volume-title":"Proc of the 3rd international workshop on safety and security in multi-agent systems (SASEMAS\u201906)","author":"P Ballarini","year":"2006","unstructured":"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\u201906)"},{"key":"183_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc of the 15th conference on foundations of software technology and theoretical computer science (FSTTCS\u201995)","author":"A Bianco","year":"1995","unstructured":"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\u201995). LNCS, vol 1026. Springer, Berlin, pp 499\u2013513"},{"key":"183_CR9","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/TIME.2008.10","volume-title":"Proc of the 15th international symposium on temporal representation and reasoning (TIME\u201908)","author":"T Brihaye","year":"2008","unstructured":"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\u201908). IEEE Press, New York, pp 32\u201340"},{"issue":"1\u20133","key":"183_CR10","doi-asserted-by":"crossref","first-page":"81","DOI":"10.3233\/FI-2009-0089","volume":"93","author":"N Bulling","year":"2009","unstructured":"Bulling N, Jamroga W (2009) What agents can probably enforce. Fundam Inform 93(1\u20133):81\u201396","journal-title":"Fundam Inform"},{"key":"183_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Proc of the 23rd international conference on computer aided verification (CAV\u201911)","author":"P Cern\u00fd","year":"2011","unstructured":"Cern\u00fd 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\u201911). LNCS, vol 6806. Springer, Berlin, pp 243\u2013259"},{"key":"183_CR12","unstructured":"Chatterjee K (2007) Stochastic \u03c9-regular games. PhD thesis, University of California at Berkeley"},{"key":"183_CR13","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 years of model checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee K, Henzinger T (2008) Value iteration. In: 25 years of model checking, pp 107\u2013138"},{"key":"183_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Proc of the 22nd international conference on computer aided verification (CAV\u201910)","author":"K Chatterjee","year":"2010","unstructured":"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\u201910). LNCS. Springer, Berlin, pp\u00a0665\u2013669"},{"key":"183_CR15","first-page":"121","volume-title":"Proc of the 15th annual ACM-SIAM symposium on discrete algorithms (SODA\u201904)","author":"K Chatterjee","year":"2004","unstructured":"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\u201904). SIAM, Philadelphia, pp 121\u2013130"},{"key":"183_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/978-3-642-28756-5_22","volume-title":"Proc of the 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201912)","author":"T Chen","year":"2012","unstructured":"Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A (2012) Automatic verification of competitive stochastic systems. In: Flanagan C, K\u00f6nig B (eds) Proc of the 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201912). LNCS, vol 7214. Springer, Berlin, pp 315\u2013330"},{"key":"183_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-3-642-22359-4_14","volume-title":"Proc of the 12th international workshop on computational logic in multi-agent systems (CLIMA XII 2011)","author":"T Chen","year":"2011","unstructured":"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\u2013297"},{"key":"183_CR18","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/FSKD.2007.458","volume-title":"Proc of the 4th international conference on fuzzy systems and knowledge discovery (FSKD\u201907)","author":"T Chen","year":"2007","unstructured":"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\u201907). IEEE Press, New York, pp 35\u201339"},{"key":"183_CR19","series-title":"DIMACS series in discrete mathematics and theoretical computer science","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume-title":"Advances in computational complexity theory","author":"A Condon","year":"1993","unstructured":"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\u201373"},{"issue":"4","key":"183_CR20","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857\u2013907","journal-title":"J ACM"},{"key":"183_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"Proc of the 10th international conference on concurrency theory (CONCUR\u201999)","author":"L Alfaro de","year":"1999","unstructured":"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\u201999). LNCS, vol 1664. Springer, Berlin, pp 66\u201381"},{"key":"183_CR22","first-page":"141","volume-title":"Proc of the 15th annual IEEE symposium on logic in computer science","author":"L Alfaro de","year":"2000","unstructured":"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\u2013154"},{"key":"183_CR23","volume-title":"Competitive Markov decision processes","author":"J Filar","year":"1997","unstructured":"Filar J, Vrieze K (1997) Competitive Markov decision processes. Springer, Berlin"},{"key":"183_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal methods for eternal networked software systems (SFM\u201911)","author":"V Forejt","year":"2011","unstructured":"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\u201911). LNCS, vol 6659. Springer, Berlin, pp 53\u2013113"},{"issue":"5","key":"183_CR25","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512\u2013535","journal-title":"Form Asp Comput"},{"key":"183_CR26","first-page":"63","volume-title":"Proc of the 8th international conference on the European energy market (EEM\u201911)","author":"H Hildmann","year":"2011","unstructured":"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\u201911), pp 63\u201368"},{"issue":"3","key":"183_CR27","doi-asserted-by":"crossref","first-page":"399","DOI":"10.3233\/JCS-2003-11307","volume":"11","author":"S Kremer","year":"2003","unstructured":"Kremer S, Raskin J-F (2003) A game-based verification of non-repudiation and fair exchange protocols. J Comput Secur 11(3):399\u2013430","journal-title":"J Comput Secur"},{"key":"183_CR28","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proc of the 23rd international conference on computer aided verification (CAV\u201911)","author":"M Kwiatkowska","year":"2011","unstructured":"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\u201911). LNCS, vol 6806. Springer, Berlin, pp 585\u2013591"},{"key":"183_CR29","series-title":"LNCS","first-page":"243","volume-title":"Proc of the 10th international conference on foundations of software science and computational structures (FOSSACS\u201907)","author":"F Laroussinie","year":"2007","unstructured":"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\u201907). LNCS, vol 4423. Springer, Berlin, pp 243\u2013257"},{"key":"183_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Proc of the 21st international conference on computer aided verification (CAV\u201909)","author":"A Lomuscio","year":"2009","unstructured":"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\u201909). LNCS, vol 5643. Springer, Berlin, pp 682\u2013688"},{"issue":"4","key":"183_CR31","doi-asserted-by":"crossref","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D Martin","year":"1998","unstructured":"Martin D (1998) The determinacy of Blackwell games. J Symb Log 63(4):1565\u20131581","journal-title":"J Symb Log"},{"key":"183_CR32","doi-asserted-by":"crossref","unstructured":"McIver A, Morgan C (2007) Results on the quantitative mu-calculus qMu. ACM Trans Comput Log 8(1). doi: 10.1145\/1182613.1182616","DOI":"10.1145\/1182613.1182616"},{"key":"183_CR33","doi-asserted-by":"crossref","unstructured":"Saffre F, Simaitis A (2012) Host selection through collective decision. ACM Trans Auton Adapt Syst 7(1). doi: 10.1145\/2168260.2168264","DOI":"10.1145\/2168260.2168264"},{"key":"183_CR34","first-page":"1057","volume-title":"Proc of the 9th international conference on autonomous agents and multiagent systems (AAMAS\u201910)","author":"H Schnoor","year":"2010","unstructured":"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\u201910), pp 1057\u20131064"},{"key":"183_CR35","doi-asserted-by":"crossref","unstructured":"Ummels M (2010) Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen University","DOI":"10.5117\/9789085550402"},{"issue":"3","key":"183_CR36","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S1090-9443(03)00031-0","volume":"57","author":"W Hoek van der","year":"2003","unstructured":"van der Hoek W, Wooldridge M (2003) Model checking cooperation, knowledge, and time\u2014a case study. Res Econ 57(3):235\u2013265","journal-title":"Res Econ"},{"key":"183_CR37","series-title":"IFIP","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-642-15240-5_6","volume-title":"Proc of the 6th IFIP conference on theoretical computer science (TCS\u201910)","author":"C Zhang","year":"2010","unstructured":"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\u201910). IFIP, vol 323. Springer, Berlin, pp\u00a071\u201385"},{"key":"183_CR38","series-title":"LNCS","first-page":"431","volume-title":"Proc of the 38th conference on current trends in theory and practice of computer science (SOFSEM\u201912)","author":"C Zhang","year":"2012","unstructured":"Zhang C, Pang J (2012) An algorithm for probabilistic alternating simulation. In: Bielikov\u00e1 M, Friedrich G, Gottlob G, Katzenbeisser S, Tur\u00e1n G (eds) Proc of the 38th conference on current trends in theory and practice of computer science (SOFSEM\u201912). LNCS, vol 7147. Springer, Berlin, pp 431\u2013442"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0183-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0183-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0183-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,22]],"date-time":"2020-07-22T10:54:53Z","timestamp":1595415293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0183-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2,16]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["183"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0183-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2,16]]}}}