{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:05:47Z","timestamp":1743113147359,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate zero-sum turn-based two-player stochastic games in which the objective of one player is to maximize the amount of rewards obtained during a play, while the other aims at minimizing it. We focus on games in which the minimizer plays in a fair way. We believe that these kinds of games enjoy interesting applications in software verification, where the maximizer plays the role of a system intending to maximize the number of \u201cmilestones\u201d achieved, and the minimizer represents the behavior of some uncooperative but yet fair environment. Normally, to study total reward properties, games are requested to be stopping (i.e., they reach a terminal state with probability 1). We relax the property to request that the game is stopping only under a fair minimizing player. We prove that these games are determined, i.e., each state of the game has a value defined. Furthermore, we show that both players have memoryless and deterministic optimal strategies, and the game value can be computed by approximating the greatest-fixed point of a set of functional equations. We implemented our approach in a prototype tool, and evaluated it on an illustrating example and an Unmanned Aerial Vehicle case study.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_3","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"48-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Playing Against Fair Adversaries in\u00a0Stochastic Games with\u00a0Total Rewards"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5835-4333","authenticated-orcid":false,"given":"Pablo F.","family":"Castro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8528-9215","authenticated-orcid":false,"given":"Pedro R.","family":"D\u2019Argenio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1651-624X","authenticated-orcid":false,"given":"Ramiro","family":"Demasi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3063-4704","authenticated-orcid":false,"given":"Luciano","family":"Putruele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: 15th Annual IEEE Symposium on Logic in Computer Science, pp. 141\u2013154. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/LICS.2000.855763","DOI":"10.1109\/LICS.2000.855763"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Asarin, E., Chane-Yack-Fa, R., Varacca, D.: Fair adversaries and randomization in two-player games. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 64\u201378. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12032-9_6","DOI":"10.1007\/978-3-642-12032-9_6"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., Bertrand, N., Dubslaff, C., Gburek, D., Sankur, O.: Stochastic shortest paths and weight-bounded properties in Markov decision processes. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 86\u201394. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209184","DOI":"10.1145\/3209108.3209184"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: L\u00e9vy, J., Mayr, E.W., Mitchell, J.C. (eds.) Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004). IFIP, vol. 155, pp. 493\u2013506. Kluwer\/Springer (2004). https:\/\/doi.org\/10.1007\/1-4020-8141-3_38","DOI":"10.1007\/1-4020-8141-3_38"},{"key":"3_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.Z.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125\u2013155 (1998). https:\/\/doi.org\/10.1007\/s004460050046","journal-title":"Distrib. Comput."},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Banerjee, T., Majumdar, R., Mallik, K., Schmuck, A., Soudjani, S.: A direct symbolic algorithm for solving stochastic Rabin games. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Proceedings, Part II. LNCS, vol. 13244, pp. 81\u201398. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_5","DOI":"10.1007\/978-3-030-99527-0_5"},{"key":"3_CR9","unstructured":"Bellman, R.: Dynamic Programming, 1st edn. Princeton University Press, Princeton (1957)"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Novotn\u00fd, P.: Determinacy in stochastic games with unbounded payoff functions. In: Ku\u010dera, A., Henzinger, T.A., Ne\u0161et\u0159il, J., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2012. LNCS, vol. 7721, pp. 94\u2013105. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36046-6_10","DOI":"10.1007\/978-3-642-36046-6_10"},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.A.: A survey of stochastic $$\\omega $$-regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.05.002","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"3_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013). https:\/\/doi.org\/10.1007\/s10703-013-0183-7","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR13","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Cai, J. (ed.) Advances in Computational Complexity Theory, Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 13, pp. 51\u201371. DIMACS\/AMS (1990)"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90048-K","journal-title":"Inf. Comput."},{"key":"3_CR15","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"D\u2019Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: Synthesis of live behaviour models for fallible domains. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011. pp. 211\u2013220. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985823","DOI":"10.1145\/1985793.1985823"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Feng, L., Wiltsche, C., Humphrey, L.R., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: Bayen, A.M., Branicky, M.S. (eds.) Proceedings of the ACM\/IEEE Sixth International Conference on Cyber-Physical Systems, ICCPS 2015, pp. 70\u201379. ACM (2015). https:\/\/doi.org\/10.1145\/2735960.2735973","DOI":"10.1145\/2735960.2735973"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/978-1-4612-4054-9","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.12.003","journal-title":"Theor. Comput. Sci."},{"key":"3_CR20","volume-title":"Linear Programming and Finite Markovian Control Problems","author":"L Kallenberg","year":"1983","unstructured":"Kallenberg, L.: Linear Programming and Finite Markovian Control Problems. Mathematisch Centrum, Amsterdam (1983)"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Ku\u010dera, A.: Turn-based stochastic games. In: Apt, K.R., Gr\u00e4del, E. (eds.) Lectures in Game Theory for Computer Scientists, pp. 146\u2013184. Cambridge University Press (2011). https:\/\/doi.org\/10.1017\/CBO9780511973468.006","DOI":"10.1017\/CBO9780511973468.006"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"3_CR23","doi-asserted-by":"publisher","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"4","key":"3_CR24","doi-asserted-by":"publisher","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"DA Martin","year":"1998","unstructured":"Martin, D.A.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565\u20131581 (1998). https:\/\/doi.org\/10.2307\/2586667","journal-title":"J. Symb. Log."},{"key":"3_CR25","unstructured":"Morgenstern, O., von Neumann, J.: Theory of Games and Economic Behavior, 1st edn. Princeton University Press (1942)"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"804","DOI":"10.1137\/S0363012996299557","volume":"37","author":"SD Patek","year":"1999","unstructured":"Patek, S.D., Bertsekas, D.P.: Stochastic shortest path games. SIAM J. Control Optimiz. 37, 804\u2013824 (1999)","journal-title":"SIAM J. Control Optimiz."},{"issue":"10","key":"3_CR27","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. 39(10), 1095\u20131100 (1953). https:\/\/doi.org\/10.1073\/pnas.39.10.1095","journal-title":"Proc. Natl. Acad. Sci."},{"key":"3_CR28","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.ejcon.2016.04.009","volume":"30","author":"M Svorenov\u00e1","year":"2016","unstructured":"Svorenov\u00e1, M., Kwiatkowska, M.: Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control 30, 15\u201330 (2016). https:\/\/doi.org\/10.1016\/j.ejcon.2016.04.009","journal-title":"Eur. J. Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:17:47Z","timestamp":1659687467000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}