{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T04:08:47Z","timestamp":1758946127181},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287558"},{"type":"electronic","value":"9783642287565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_22","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:57:15Z","timestamp":1332435435000},"page":"315-330","source":"Crossref","is-referenced-by-count":22,"title":["Automatic Verification of Competitive Stochastic Systems"],"prefix":"10.1007","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Aistis","family":"Simaitis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-642-04444-1_35","volume-title":"Computer Security \u2013 ESORICS 2009","author":"M. Aizatulin","year":"2009","unstructured":"Aizatulin, M., Schnoor, H., Wilke, T.: Computationally Sound Analysis of a Probabilistic Contract Signing Protocol. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol.\u00a05789, pp. 571\u2013586. Springer, Heidelberg (2009)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999. Concurrency Theory","author":"L. Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing Minimum and Maximum Reachability Times in Probabilistic Systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, p. 66. Springer, Heidelberg (1999)"},{"key":"22_CR3","unstructured":"de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: LICS (2000)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in Model Checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"issue":"5","key":"22_CR5","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Br\u00e1zdil, T., Gr\u00f6\u00dfer, M., Kucera, A.: Stochastic game logic. In: Proc. QEST 2007, pp. 227\u2013236. IEEE (2007)","DOI":"10.1109\/QEST.2007.38"},{"key":"22_CR7","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-04879-1_12","volume-title":"Safety and Security in Multiagent Systems","author":"P. Ballarini","year":"2009","unstructured":"Ballarini, P., Fisher, M., Wooldridge, M.: Uncertain Agent Verification through Probabilistic Model-Checking. In: Barley, M., Mouratidis, H., Unruh, A., Spears, D., Scerri, P., Massacci, F. (eds.) SASEMAS 2004-2006. LNCS, vol.\u00a04324, pp. 162\u2013174. Springer, Heidelberg (2009)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P. \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative Synthesis for Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 243\u2013259. Springer, Heidelberg (2011)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Computer Aided Verification","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: A Solver for Probabilistic Games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 665\u2013669. Springer, Heidelberg (2010)"},{"key":"22_CR11","unstructured":"Chatterjee, K.: Stochastic \u03c9-Regular Games. Ph.D. thesis (2007)"},{"key":"22_CR12","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Tech. Rep. RR-11-11, University of Oxford (2011)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-22359-4_14","volume-title":"Computational Logic in Multi-Agent Systems","author":"T. Chen","year":"2011","unstructured":"Chen, T., Kwiatkowska, M., Parker, D., Simaitis, A.: Verifying Team Formation Protocols with Probabilistic Model Checking. In: Leite, J., Torroni, P., \u00c5gotnes, T., Boella, G., van der Torre, L. (eds.) CLIMA XII 2011. LNCS, vol.\u00a06814, pp. 190\u2013207. Springer, Heidelberg (2011)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: Proc. FSKD 2007, pp. 35\u201339. IEEE (2007)","DOI":"10.1109\/FSKD.2007.458"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory. DIMACS, vol.\u00a013, pp. 51\u201373 (1993)","DOI":"10.1090\/dimacs\/013\/04"},{"key":"22_CR16","volume-title":"Competitive Markov Decision Processes","author":"J. Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 53\u2013113. Springer, Heidelberg (2011)"},{"issue":"5","key":"22_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Hildmann, H., Saffre, F.: Influence of variable supply and load flexibility on demand-side management. In: Proc. EEM 2011, pp. 63\u201368 (2011)","DOI":"10.1109\/EEM.2011.5952980"},{"issue":"3","key":"22_CR20","doi-asserted-by":"publisher","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.: Model checking cooperation, knowledge, and time - A case study. Research In Economics\u00a057(3), 235\u2013265 (2003)","journal-title":"Research In Economics"},{"issue":"3","key":"22_CR21","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.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security\u00a011(3), 399\u2013430 (2003)","journal-title":"Journal of Computer Security"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A. Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Martin, D.: The determinacy of Blackwell games. J. Symb. Log.\u00a063(4) (1998)","DOI":"10.2307\/2586667"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic\u00a08(1) (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Saffre, F., Simaitis, A.: Host selection through collective decision. ACM Transactions on Autonomous and Adaptive Systems, TAAS (to appear, 2012)","DOI":"10.1145\/2168260.2168264"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Ummels, M.: Stochastic Multiplayer Games: Theory and Algorithms. Ph.D. thesis, RWTH Aachen University (2010)","DOI":"10.5117\/9789085550402"},{"key":"22_CR28","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15240-5_6","volume-title":"Theoretical Computer Science","author":"C. Zhang","year":"2010","unstructured":"Zhang, C., Pang, J.: On Probabilistic Alternating Simulations. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol.\u00a0323, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"22_CR29","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/tacas12smg\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:08:50Z","timestamp":1620112130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}