{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:19:13Z","timestamp":1742966353370,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03c9<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy level<jats:italic>k<\/jats:italic>, is decidable and in<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {NP}\\cap \\mathsf {coNP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>NP<\/mml:mi><mml:mo>\u2229<\/mml:mo><mml:mi>coNP<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The same holds for checking if such a<jats:italic>k<\/jats:italic>exists and if a given<jats:italic>k<\/jats:italic>is minimal.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_22","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"427-447","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP"],"prefix":"10.1007","author":[{"given":"Richard","family":"Mayr","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9093-9518","authenticated-orcid":false,"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5274-8190","authenticated-orcid":false,"given":"Patrick","family":"Totzke","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5560-0546","authenticated-orcid":false,"given":"Dominik","family":"Wojtczak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: International Conference on Concurrency Theory (CONCUR). vol. 8052 (2013)","DOI":"10.1007\/978-3-642-40184-8_9"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Ciobanu, R., Mayr, R., Sangnier, A., Sproston, J.: Qualitative analysis of VASS-induced MDPs. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). vol. 9634 (2016)","DOI":"10.1007\/978-3-662-49630-5_19"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Mayr, R.: Decisive Markov Chains. Logical Methods in Computer Science Volume 3, Issue 4 (Nov 2007)","DOI":"10.2168\/LMCS-3(4:7)2007"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J.\u00a0ACM 49(5), 672\u2013713 (2002)","DOI":"10.1145\/585265.585270"},{"key":"22_CR5","unstructured":"Billingsley, P.: Probability and Measure. Wiley (1995), third Edition"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theory of Computing systems 36(3) (2003)","DOI":"10.1007\/s00224-003-1061-2"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). vol. 5215, pp. 33\u201347 (2008)","DOI":"10.1007\/978-3-540-85778-5_4"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Etessami, K., Ku\u010dera, A.: Approximating the Termination Value of One-Counter MDPs and Stochastic Games. Information and Computation 222, 121\u2013138 (2013)","DOI":"10.1016\/j.ic.2012.01.008"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Novotn\u00fd, P.: Optimizing the expected mean payoff in energy Markov decision processes. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). vol. 9938, pp. 32\u201349 (2016)","DOI":"10.1007\/978-3-319-46520-3_3"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V., Ku\u010dera,A.: Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science 10 (2014)","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"22_CR11","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Etessami, K.: One-Counter Stochastic Games. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). vol.\u00a08, pp. 108\u2013119 (2010)"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Etessami, K., Ku\u010dera, A., Wojtczak,D.: One-counter Markov decision processes. In: ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 863\u2013874 (2010)","DOI":"10.1137\/1.9781611973075.70"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Kiefer, S., Ku\u010dera, A., Novotn\u00fd, P., Katoen, J.P.: Zero-reachability in probabilistic multi-counter automata. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 22:1\u201322:10 (2014)","DOI":"10.1145\/2603088.2603161"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Chakrabarti, A., De\u00a0Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: International Workshop on Embedded Software. pp. 117\u2013133 (2003)","DOI":"10.1007\/978-3-540-45212-6_9"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., De\u00a0Alfaro, L., Henzinger, T.A.: The complexity of stochastic Rabin and Streett games. In: International Colloquium on Automata, Languages and Programming (ICALP). pp. 878\u2013890 (2005)","DOI":"10.1007\/11523468_71"},{"key":"22_CR16","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. In: International Colloquium on Automata, Languages and Programming (ICALP). vol. 6199, pp. 599\u2013610 (2010)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Energy and mean-payoff parity Markov decision processes. In: International Symposium on Mathematical Foundations of Computer Science (MFCS). vol. 6907, pp. 206\u2013218 (2011)","DOI":"10.1007\/978-3-642-22993-0_21"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Games and Markov decision processes with mean-payoff parity and energy parity objectives. In: Mathematical and Engineering Methods in Computer Science (MEMICS). LNCS, vol. 7119, pp. 37\u201346. Springer (2011)","DOI":"10.1007\/978-3-642-25929-6_3"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. Theoretical Computer Science 458, 49\u201360 (2012)","DOI":"10.1016\/j.tcs.2012.07.038"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Gimbert, H., Oualhadj, Y.: Perfect-information stochastic mean-payoff parity games. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). vol. 8412 (2014)","DOI":"10.1007\/978-3-642-54830-7_14"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). pp. 153\u2013167 (2007)","DOI":"10.1007\/978-3-540-71389-0_12"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.A.: Simple stochastic parity games. In: Computer Science Logic (CSL). vol. 2803, pp. 100\u2013113. Springer (2003)","DOI":"10.1007\/978-3-540-45220-1_11"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 121\u2013130. SIAM (2004)","DOI":"10.21236\/ADA603293"},{"key":"22_CR24","unstructured":"Chatterjee, K., Kret\u00ednsk\u00e1, Z., Kret\u00ednsk\u00fd, J.:Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science 13(2) (2017)"},{"key":"22_CR25","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (Dec 1999)"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Daviaud, L., Jurdzi\u0144ski, M., Lazi\u0107, R.: A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In: Logic in Computer Science (LICS). pp. 325\u2013334 (2018)","DOI":"10.1145\/3209108.3209162"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"De\u00a0Alfaro, L., Henzinger, T.A.: Interface automata. ACM SIGSOFT Software Engineering Notes 26(5), 109\u2013120 (2001)","DOI":"10.1145\/503271.503226"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits, vol.\u00a024. MIT press Cambridge (1989)","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Fearnley, J.: Exponential lower bounds for policy iteration. In: International Colloquium on Automata, Languages and Programming (ICALP). pp. 551\u2013562 (2010)","DOI":"10.1007\/978-3-642-14162-1_46"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: Logic in Computer Science (LICS). pp. 145\u2013156 (2009)","DOI":"10.1109\/LICS.2009.27"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Friedmann, O., Hansen, T.D., Zwick, U.: Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In: Symposium on Theory of Computing (STOC). pp. 283\u2013292 (2011)","DOI":"10.1145\/1993636.1993675"},{"key":"22_CR33","unstructured":"Gillette, D.: Stochastic games with zero stop probabilities. Contributions to the Theory of Games 3, 179\u2013187 (1957)"},{"key":"22_CR34","unstructured":"Gimbert, H., Kelmendi, E.: Two-Player Perfect-Information Shift-Invariant Submixing Stochastic Games Are Half-Positional (Jan 2014), working paper or preprint available at: https:\/\/hal.archives-ouvertes.fr\/hal-00936371"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in UP $$\\cap $$ co-UP. Information Processing Letters 68(3), 119\u2013124 (1998)","DOI":"10.1016\/S0020-0190(98)00150-1"},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Lazi\u0107, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: International Colloquium on Automata, Languages and Programming (ICALP). vol. 9135, pp. 260\u2013272 (2015)","DOI":"10.1007\/978-3-662-47666-6_21"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Kiefer, S., Mayr, R., Shirmohammadi, M., Wojtczak, D.: On strong determinacy of countable stochastic games. Logic in Computer Science (LICS) (2017)","DOI":"10.1109\/LICS.2017.8005134"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"Maitra, A., Sudderth, W.: Stochastic games with Borel payoffs. In: Stochastic Games and Applications, pp. 367\u2013373. Kluwer, Dordrecht (2003)","DOI":"10.1007\/978-94-010-0189-2_24"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"Martin, D.A.: The determinacy of Blackwell games. Journal of Symbolic Logic 63(4), 1565\u20131581 (1998)","DOI":"10.2307\/2586667"},{"key":"22_CR40","doi-asserted-by":"crossref","unstructured":"Mayr, R., Schewe, S., Totzke, P., Wojtczak, D.: MDPs with Energy-Parity Objectives. Logic in Computer Science (LICS) (2017)","DOI":"10.1109\/LICS.2017.8005131"},{"key":"22_CR41","unstructured":"Mayr, R., Schewe, S., Totzke, P., Wojtczak, D.: Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP (2021), arXiv:2101.06989"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Annual Symposium on Principles of Programming Languages (POPL). pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"22_CR43","doi-asserted-by":"crossref","unstructured":"Pogosyants, A., Segala, R., Lynch, N.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing 13(3), 155\u2013186 (2000)","DOI":"10.1007\/PL00008917"},{"key":"22_CR44","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on infinite objects and Church\u2019s problem, vol.\u00a013. American Mathematical Soc. (1972)","DOI":"10.1090\/cbms\/013"},{"key":"22_CR45","doi-asserted-by":"crossref","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM journal on control and optimization 25(1), 206\u2013230 (1987)","DOI":"10.1137\/0325013"},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"Shapley, L.S.: Stochastic games. Proceedings of the national academy of sciences 39(10), 1095\u20131100 (1953)","DOI":"10.1073\/pnas.39.10.1953"},{"key":"22_CR47","doi-asserted-by":"crossref","unstructured":"Stoelinga, M.: Fun with firewire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal aspects of computing 14(3), 328\u2013337 (2003)","DOI":"10.1007\/s001650300009"},{"key":"22_CR48","doi-asserted-by":"crossref","unstructured":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A., Raskin, J.F.: The complexity of multi-mean-payoff and multi-energy games. Information and Computation 241, 177 \u2013 196 (2015)","DOI":"10.1016\/j.ic.2015.03.001"},{"key":"22_CR49","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Alternating tree automata, parity games, and modal mu-calculus. Bulletin of the Belgian Mathematical Society Simon Stevin 8(2), 359 (2001)","DOI":"10.36045\/bbms\/1102714178"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:35:22Z","timestamp":1671683722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"88","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":"28","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":"0","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":"32% - 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,2","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}