[{"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","intvolume":"        66","date_created":"2019-08-04T21:59:16Z","article_number":"31","department":[{"_id":"ToHe"}],"isi":1,"volume":66,"month":"07","quality_controlled":"1","publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]},"type":"journal_article","language":[{"iso":"eng"}],"doi":"10.1145/3340295","publisher":"ACM","year":"2019","date_published":"2019-07-16T00:00:00Z","author":[{"first_name":"Guy","full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K"}],"oa":1,"_id":"6752","issue":"4","scopus_import":"1","project":[{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","call_identifier":"FWF"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","call_identifier":"FWF"}],"citation":{"chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games.” <i>Journal of the ACM</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3340295\">https://doi.org/10.1145/3340295</a>.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” <i>Journal of the ACM</i>, vol. 66, no. 4. ACM, 2019.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","apa":"Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2019). Infinite-duration bidding games. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3340295\">https://doi.org/10.1145/3340295</a>","mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” <i>Journal of the ACM</i>, vol. 66, no. 4, 31, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3340295\">10.1145/3340295</a>.","ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. <i>Journal of the ACM</i>. 2019;66(4). doi:<a href=\"https://doi.org/10.1145/3340295\">10.1145/3340295</a>"},"arxiv":1,"publication":"Journal of the ACM","external_id":{"arxiv":["1705.01433"],"isi":["000487714900008"]},"related_material":{"record":[{"relation":"earlier_version","id":"950","status":"public"}]},"title":"Infinite-duration bidding games","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.01433"}],"status":"public","date_updated":"2023-08-29T07:02:13Z","publication_status":"published","oa_version":"Preprint","day":"16","abstract":[{"text":"Two-player games on graphs are widely studied in formal methods, as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. The following bidding rule was previously defined and called Richman bidding. Both players have separate budgets, which sum up to 1. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a threshold budget in a vertex is a value t ∈ [0, 1] such that if Player 1’s budget exceeds t, he can win the game; and if Player 2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with random-turn games—a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players.","lang":"eng"}]},{"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1201.2829"}],"external_id":{"arxiv":["1201.2829"]},"title":"The complexity of mean-payoff pushdown games","publication":"Journal of the ACM","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"}],"citation":{"apa":"Chatterjee, K., &#38; Velner, Y. (2017). The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>","mla":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>, vol. 64, no. 5, ACM, 2017, p. 34, doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>.","short":"K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.","ista":"Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games. Journal of the ACM. 64(5), 34.","ama":"Chatterjee K, Velner Y. The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. 2017;64(5):34. doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>.","ieee":"K. Chatterjee and Y. Velner, “The complexity of mean-payoff pushdown games,” <i>Journal of the ACM</i>, vol. 64, no. 5. ACM, p. 34, 2017."},"arxiv":1,"issue":"5","scopus_import":1,"ec_funded":1,"abstract":[{"lang":"eng","text":"Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion.While pushdown games have been studied before with qualitative objectives-such as reachability and ?-regular objectives- in this work, we study for the first time such games with the most well-studied quantitative objective, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity by showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games and memoryless modular strategies are sufficient in two-player pushdown games. Finally, we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded."}],"oa_version":"Preprint","publication_status":"published","page":"34","day":"01","date_updated":"2021-01-12T08:12:08Z","status":"public","quality_controlled":"1","publication_identifier":{"issn":["00045411"]},"publist_id":"6964","month":"09","volume":64,"article_type":"original","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:48:06Z","intvolume":"        64","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"_id":"716","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"date_published":"2017-09-01T00:00:00Z","publisher":"ACM","year":"2017","language":[{"iso":"eng"}],"doi":"10.1145/3121408","type":"journal_article"}]