[{"volume":17,"article_type":"original","isi":1,"publication_identifier":{"eissn":["1860-5974"]},"quality_controlled":"1","month":"02","intvolume":"        17","keyword":["computer science","computer science and game theory","logic in computer science"],"file_date_updated":"2022-01-26T08:04:50Z","ddc":["510"],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","article_processing_charge":"No","department":[{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).\r\n","date_created":"2022-01-25T16:32:13Z","date_published":"2021-02-03T00:00:00Z","_id":"10674","oa":1,"author":[{"last_name":"Aghajohari","full_name":"Aghajohari, Milad","first_name":"Milad"},{"full_name":"Avni, Guy","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"type":"journal_article","year":"2021","publisher":"International Federation for Computational Logic","doi":"10.23638/LMCS-17(1:10)2021","language":[{"iso":"eng"}],"file":[{"creator":"alisjak","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_size":819878,"file_name":"2021_LMCS_AGHAJOHAR.pdf","date_updated":"2022-01-26T08:04:50Z","success":1,"file_id":"10690","checksum":"b35586a50ed1ca8f44767de116d18d81","date_created":"2022-01-26T08:04:50Z"}],"title":"Determinacy in discrete-bidding infinite-duration games","external_id":{"isi":["000658724600010"],"arxiv":["1905.03588"]},"publication":"Logical Methods in Computer Science","has_accepted_license":"1","scopus_import":"1","issue":"1","citation":{"chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2021. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2021). Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>","short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","ista":"Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.","mla":"Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1, International Federation for Computational Logic, 2021, p. 10:1-10:23, doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>.","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. 2021;17(1):10:1-10:23. doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>"},"arxiv":1,"project":[{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"}],"abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets."}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"day":"03","oa_version":"Published Version","publication_status":"published","page":"10:1-10:23","status":"public","date_updated":"2023-08-17T06:56:42Z"},{"abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"day":"06","oa_version":"Submitted Version","publication_status":"published","page":"42-55","date_updated":"2023-08-17T13:52:49Z","status":"public","file":[{"relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"dernst","date_updated":"2020-10-09T06:31:22Z","success":1,"checksum":"e86635417f45eb2cd75778f91382f737","file_id":"8639","date_created":"2020-10-09T06:31:22Z","file_size":1413001,"file_name":"2020_TheoreticalCS_Avni.pdf"}],"title":"Dynamic resource allocation games","related_material":{"record":[{"status":"public","id":"1341","relation":"earlier_version"}]},"external_id":{"isi":["000512219400004"]},"publication":"Theoretical Computer Science","citation":{"chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” <i>Theoretical Computer Science</i>, vol. 807. Elsevier, pp. 42–55, 2020.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2020). Dynamic resource allocation games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>","short":"G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020) 42–55.","mla":"Avni, Guy, et al. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>, vol. 807, Elsevier, 2020, pp. 42–55, doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>.","ista":"Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games. Theoretical Computer Science. 807, 42–55.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. <i>Theoretical Computer Science</i>. 2020;807:42-55. doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>"},"project":[{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"has_accepted_license":"1","scopus_import":"1","_id":"6761","oa":1,"author":[{"full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"date_published":"2020-02-06T00:00:00Z","year":"2020","publisher":"Elsevier","doi":"10.1016/j.tcs.2019.06.031","language":[{"iso":"eng"}],"type":"journal_article","publication_identifier":{"issn":["03043975"]},"quality_controlled":"1","month":"02","volume":807,"article_type":"original","isi":1,"department":[{"_id":"ToHe"}],"date_created":"2019-08-04T21:59:20Z","intvolume":"       807","file_date_updated":"2020-10-09T06:31:22Z","article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","ddc":["000"]},{"project":[{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF"}],"arxiv":1,"citation":{"ieee":"G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805, 2020.","chicago":"Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>.","ama":"Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2020;34(02):1798-1805. doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>","short":"G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference on Artificial Intelligence 34 (2020) 1798–1805.","mla":"Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02, Association for the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>.","ista":"Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805.","apa":"Avni, G., Ibsen-Jensen, R., &#38; Tkadlec, J. (2020). All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>"},"issue":"02","scopus_import":"1","external_id":{"arxiv":["1911.08360"]},"title":"All-pay bidding games on graphs","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","date_updated":"2023-09-05T12:40:00Z","status":"public","abstract":[{"lang":"eng","text":"In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve."}],"oa_version":"Preprint","publication_status":"published","page":"1798-1805","day":"03","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"acknowledgement":"This research was supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).","date_created":"2021-02-25T09:05:18Z","intvolume":"        34","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","conference":{"start_date":"2020-02-07","end_date":"2020-02-12","name":"AAAI: Conference on Artificial Intelligence","location":"New York, NY, United States"},"quality_controlled":"1","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"],"isbn":["9781577358350"]},"month":"04","volume":34,"article_type":"original","publisher":"Association for the Advancement of Artificial Intelligence","year":"2020","language":[{"iso":"eng"}],"doi":"10.1609/aaai.v34i02.5546","type":"journal_article","_id":"9197","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Tkadlec, Josef","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","orcid":"0000-0002-1097-9684"}],"date_published":"2020-04-03T00:00:00Z"},{"abstract":[{"lang":"eng","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."}],"day":"16","publication_status":"published","oa_version":"Preprint","status":"public","date_updated":"2023-08-29T07:02:13Z","title":"Infinite-duration bidding games","external_id":{"isi":["000487714900008"],"arxiv":["1705.01433"]},"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"950"}]},"publication":"Journal of the ACM","main_file_link":[{"url":"https://arxiv.org/abs/1705.01433","open_access":"1"}],"scopus_import":"1","issue":"4","citation":{"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>","short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31.","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>.","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>","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.","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>."},"arxiv":1,"project":[{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23"},{"call_identifier":"FWF","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory"}],"date_published":"2019-07-16T00:00:00Z","_id":"6752","oa":1,"author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K"}],"type":"journal_article","year":"2019","publisher":"ACM","doi":"10.1145/3340295","language":[{"iso":"eng"}],"volume":66,"isi":1,"publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]},"quality_controlled":"1","month":"07","intvolume":"        66","article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","department":[{"_id":"ToHe"}],"date_created":"2019-08-04T21:59:16Z","article_number":"31"},{"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2019-09-11","end_date":"2019-09-13","name":"RP: Reachability Problems","location":"Brussels, Belgium"},"file_date_updated":"2020-07-14T12:47:41Z","intvolume":"     11674","date_created":"2019-08-19T07:58:10Z","department":[{"_id":"ToHe"}],"volume":11674,"month":"09","quality_controlled":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["978-303030805-6"]},"type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-30806-3_1","publisher":"Springer","year":"2019","date_published":"2019-09-06T00:00:00Z","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr"}],"oa":1,"_id":"6822","scopus_import":1,"alternative_title":["LNCS"],"has_accepted_license":"1","project":[{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369"},{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"citation":{"ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: <i> Proceedings of the 13th International Conference of Reachability Problems</i>. Vol 11674. Springer; 2019:1-12. doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” <i> Proceedings of the 13th International Conference of Reachability Problems</i>, vol. 11674, Springer, 2019, pp. 1–12, doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:,  Proceedings of the 13th International Conference of Reachability Problems, Springer, 2019, pp. 1–12.","apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., &#38; Novotny, P. (2019). Bidding games on Markov decision processes. In <i> Proceedings of the 13th International Conference of Reachability Problems</i> (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>","ista":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov decision processes.  Proceedings of the 13th International Conference of Reachability Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in <i> Proceedings of the 13th International Conference of Reachability Problems</i>, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In <i> Proceedings of the 13th International Conference of Reachability Problems</i>, 11674:1–12. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>."},"publication":" Proceedings of the 13th International Conference of Reachability Problems","file":[{"file_size":436635,"file_name":"prob.pdf","date_updated":"2020-07-14T12:47:41Z","file_id":"6823","date_created":"2019-08-19T07:56:40Z","checksum":"45ebbc709af2b247d28c7c293c01504b","creator":"gavni","relation":"main_file","content_type":"application/pdf","access_level":"open_access"}],"title":"Bidding games on Markov decision processes","status":"public","date_updated":"2021-01-12T08:09:12Z","oa_version":"Submitted Version","publication_status":"published","page":"1-12","day":"06","abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher\r\nbidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called \r\n randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one.","lang":"eng"}]},{"date_updated":"2023-08-07T14:08:34Z","status":"public","abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the \"bank\" rather than the other player. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding. ","lang":"eng"}],"ec_funded":1,"day":"01","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publication_status":"published","oa_version":"Published Version","arxiv":1,"citation":{"ista":"Avni G, Henzinger TA, Zikelic D. 2019. Bidding mechanisms in graph games. MFCS: nternational Symposium on Mathematical Foundations of Computer Science, LIPIcs, vol. 138, 11.","short":"G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","mla":"Avni, Guy, et al. <i>Bidding Mechanisms in Graph Games</i>. Vol. 138, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">10.4230/LIPICS.MFCS.2019.11</a>.","apa":"Avni, G., Henzinger, T. A., &#38; Zikelic, D. (2019). Bidding mechanisms in graph games (Vol. 138). Presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">https://doi.org/10.4230/LIPICS.MFCS.2019.11</a>","ama":"Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">10.4230/LIPICS.MFCS.2019.11</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">https://doi.org/10.4230/LIPICS.MFCS.2019.11</a>.","ieee":"G. Avni, T. A. Henzinger, and D. Zikelic, “Bidding mechanisms in graph games,” presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany, 2019, vol. 138."},"project":[{"grant_number":"665385","call_identifier":"H2020","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"},{"grant_number":"M02369","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23"}],"has_accepted_license":"1","alternative_title":["LIPIcs"],"scopus_import":1,"title":"Bidding mechanisms in graph games","file":[{"creator":"kschuh","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":554457,"file_name":"2019_LIPIcs_Avni.pdf","date_updated":"2020-07-14T12:47:42Z","checksum":"6346e116a4f4ed1414174d96d2c4fbd7","date_created":"2019-09-27T11:45:15Z","file_id":"6913"}],"related_material":{"record":[{"relation":"later_version","id":"9239","status":"public"}]},"external_id":{"arxiv":["1905.03835"]},"year":"2019","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPICS.MFCS.2019.11","language":[{"iso":"eng"}],"type":"conference","_id":"6884","oa":1,"author":[{"orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Dorde","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic"}],"date_published":"2019-08-01T00:00:00Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2019-09-18T08:04:26Z","article_number":"11","intvolume":"       138","conference":{"location":"Aachen, Germany","end_date":"2019-08-30","start_date":"2019-08-26","name":"MFCS: nternational Symposium on Mathematical Foundations of Computer Science"},"file_date_updated":"2020-07-14T12:47:42Z","ddc":["004"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","month":"08","volume":138},{"project":[{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","call_identifier":"FWF"}],"citation":{"ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>","ista":"Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding infinite-duration games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 20.","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2019). Determinacy in discrete-bidding infinite-duration games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","mla":"Aghajohari, Milad, et al. <i>Determinacy in Discrete-Bidding Infinite-Duration Games</i>. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>."},"arxiv":1,"alternative_title":["LIPIcs"],"has_accepted_license":"1","scopus_import":"1","external_id":{"arxiv":["1905.03588"]},"title":"Determinacy in discrete-bidding infinite-duration games","file":[{"creator":"kschuh","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":741425,"file_name":"2019_LIPIcs_Aghajohari.pdf","date_updated":"2020-07-14T12:47:43Z","checksum":"4df6d3575c506edb17215adada03cc8e","file_id":"6915","date_created":"2019-09-27T12:21:38Z"}],"date_updated":"2022-01-26T08:27:10Z","license":"https://creativecommons.org/licenses/by/3.0/","status":"public","abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets. "}],"oa_version":"Published Version","publication_status":"published","day":"01","tmp":{"image":"/images/cc_by.png","short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"department":[{"_id":"ToHe"}],"date_created":"2019-09-18T08:06:58Z","article_number":"20","intvolume":"       140","ddc":["000"],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","file_date_updated":"2020-07-14T12:47:43Z","conference":{"end_date":"2019-08-30","start_date":"2019-08-27","name":"CONCUR: International Conference on Concurrency Theory","location":"Amsterdam, Netherlands"},"quality_controlled":"1","month":"08","volume":140,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2019","language":[{"iso":"eng"}],"doi":"10.4230/LIPICS.CONCUR.2019.20","type":"conference","oa":1,"_id":"6886","author":[{"last_name":"Aghajohari","first_name":"Milad","full_name":"Aghajohari, Milad"},{"orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy","first_name":"Guy"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2019-08-01T00:00:00Z"},{"volume":11561,"isi":1,"quality_controlled":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"month":"07","intvolume":"     11561","article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","ddc":["000"],"conference":{"location":"New York, NY, United States","end_date":"2019-07-18","start_date":"2019-07-13","name":"CAV: Computer Aided Verification"},"file_date_updated":"2020-07-14T12:47:31Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2019-05-16T11:22:30Z","date_published":"2019-07-12T00:00:00Z","oa":1,"_id":"6462","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy"},{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Bettina","full_name":"Konighofer, Bettina","last_name":"Konighofer"},{"last_name":"Pranger","first_name":"Stefan","full_name":"Pranger, Stefan"}],"type":"conference","publisher":"Springer","year":"2019","language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-25540-4_36","external_id":{"isi":["000491468000036"]},"title":"Run-time optimization for learned controllers through quantitative games","file":[{"access_level":"open_access","content_type":"application/pdf","relation":"main_file","creator":"dernst","file_id":"6816","checksum":"c231579f2485c6fd4df17c9443a4d80b","date_created":"2019-08-14T09:35:24Z","date_updated":"2020-07-14T12:47:31Z","file_name":"2019_CAV_Avni.pdf","file_size":659766}],"publication":"31st International Conference on Computer-Aided Verification","alternative_title":["LNCS"],"has_accepted_license":"1","scopus_import":"1","project":[{"_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","grant_number":"M02369"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"}],"citation":{"chicago":"Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers through Quantitative Games.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:630–49. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>.","ieee":"G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger, “Run-time optimization for learned controllers through quantitative games,” in <i>31st International Conference on Computer-Aided Verification</i>, New York, NY, United States, 2019, vol. 11561, pp. 630–649.","apa":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &#38; Pranger, S. (2019). Run-time optimization for learned controllers through quantitative games. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">https://doi.org/10.1007/978-3-030-25540-4_36</a>","short":"G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 630–649.","mla":"Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative Games.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 630–49, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>.","ista":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019. Run-time optimization for learned controllers through quantitative games. 31st International Conference on Computer-Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 11561, 630–649.","ama":"Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time optimization for learned controllers through quantitative games. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:630-649. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_36\">10.1007/978-3-030-25540-4_36</a>"},"abstract":[{"lang":"eng","text":"A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive  synthesis.  First,  we  abstract  the  plant  by  building  a  stochastic  model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles."}],"page":"630-649","publication_status":"published","oa_version":"Published Version","day":"12","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","date_updated":"2023-08-25T10:33:27Z"},{"date_published":"2018-11-21T00:00:00Z","_id":"5788","oa":1,"author":[{"full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"}],"type":"conference","year":"2018","publisher":"Springer","doi":"10.1007/978-3-030-04612-5_2","language":[{"iso":"eng"}],"volume":11316,"isi":1,"publication_identifier":{"isbn":["9783030046118"],"issn":["03029743"]},"quality_controlled":"1","month":"11","intvolume":"     11316","conference":{"location":"Oxford, UK","end_date":"2018-12-17","start_date":"2018-12-15","name":"14th International Conference on Web and Internet Economics, WINE"},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"ToHe"}],"date_created":"2018-12-30T22:59:14Z","abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner or payoff of the game. Such games are central in formal verification since they model the interaction between a non-terminating system and its environment. We study bidding games in which the players bid for the right to move the token. Two bidding rules have been defined. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the “bank” rather than the other player. While poorman reachability games have been studied before, we present, for the first time, results on infinite-duration poorman games. A central quantity in these games is the ratio between the two players’ initial budgets. The questions we study concern a necessary and sufficient ratio with which a player can achieve a goal. For reachability objectives, such threshold ratios are known to exist for both bidding rules. We show that the properties of poorman reachability games extend to complex qualitative objectives such as parity, similarly to the Richman case. Our most interesting results concern quantitative poorman games, namely poorman mean-payoff games, where we construct optimal strategies depending on the initial ratio, by showing a connection with random-turn based games. The connection in itself is interesting, because it does not hold for reachability poorman games. We also solve the complexity problems that arise in poorman bidding games.","lang":"eng"}],"day":"21","page":"21-36","oa_version":"Preprint","status":"public","date_updated":"2023-09-12T07:44:01Z","title":"Infinite-duration poorman-bidding games","external_id":{"arxiv":["1804.04372"],"isi":["000865933000002"]},"main_file_link":[{"url":"https://arxiv.org/abs/1804.04372","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":"1","citation":{"ista":"Avni G, Henzinger TA, Ibsen-Jensen R. 2018. Infinite-duration poorman-bidding games. 14th International Conference on Web and Internet Economics, WINE, LNCS, vol. 11316, 21–36.","mla":"Avni, Guy, et al. <i>Infinite-Duration Poorman-Bidding Games</i>. Vol. 11316, Springer, 2018, pp. 21–36, doi:<a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">10.1007/978-3-030-04612-5_2</a>.","apa":"Avni, G., Henzinger, T. A., &#38; Ibsen-Jensen, R. (2018). Infinite-duration poorman-bidding games (Vol. 11316, pp. 21–36). Presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">https://doi.org/10.1007/978-3-030-04612-5_2</a>","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R. Infinite-duration poorman-bidding games. In: Vol 11316. Springer; 2018:21-36. doi:<a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">10.1007/978-3-030-04612-5_2</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Rasmus Ibsen-Jensen. “Infinite-Duration Poorman-Bidding Games,” 11316:21–36. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-04612-5_2\">https://doi.org/10.1007/978-3-030-04612-5_2</a>.","ieee":"G. Avni, T. A. Henzinger, and R. Ibsen-Jensen, “Infinite-duration poorman-bidding games,” presented at the 14th International Conference on Web and Internet Economics, WINE, Oxford, UK, 2018, vol. 11316, pp. 21–36."},"arxiv":1,"project":[{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"M02369","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory"}]},{"department":[{"_id":"ToHe"}],"article_number":"23","date_created":"2019-02-14T14:12:09Z","intvolume":"       117","file_date_updated":"2020-07-14T12:47:15Z","conference":{"location":"Liverpool, United Kingdom","end_date":"2018-08-31","start_date":"2018-08-27","name":"MFCS: Mathematical Foundations of Computer Science"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"article_processing_charge":"No","publication_identifier":{"issn":["1868-8969"]},"quality_controlled":"1","month":"08","volume":117,"year":"2018","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPICS.MFCS.2018.23","language":[{"iso":"eng"}],"type":"conference","_id":"6005","oa":1,"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy"},{"first_name":"Shibashis","full_name":"Guha, Shibashis","last_name":"Guha"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"date_published":"2018-08-01T00:00:00Z","citation":{"mla":"Avni, Guy, et al. <i>Timed Network Games with Clocks</i>. Vol. 117, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">10.4230/LIPICS.MFCS.2018.23</a>.","apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2018). Timed network games with clocks (Vol. 117). Presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">https://doi.org/10.4230/LIPICS.MFCS.2018.23</a>","ista":"Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">10.4230/LIPICS.MFCS.2018.23</a>","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2018.23\">https://doi.org/10.4230/LIPICS.MFCS.2018.23</a>.","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom, 2018, vol. 117."},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"},{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF"}],"has_accepted_license":"1","alternative_title":["LIPIcs"],"scopus_import":"1","file":[{"content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"dernst","date_updated":"2020-07-14T12:47:15Z","date_created":"2019-02-14T14:22:04Z","file_id":"6007","checksum":"41ab2ae9b63f5eb49fa995250c0ba128","file_size":542889,"file_name":"2018_LIPIcs_Avni.pdf"}],"title":"Timed network games with clocks","related_material":{"record":[{"id":"963","status":"public","relation":"earlier_version"}]},"date_updated":"2023-02-23T14:02:58Z","status":"public","abstract":[{"lang":"eng","text":"Network games are widely used as a model for selfish resource-allocation problems. In the classicalmodel, each player selects a path connecting her source and target vertices. The cost of traversingan edge depends on theload; namely, number of players that traverse it. Thus, it abstracts the factthat different users may use a resource at different times and for different durations, which playsan important role in determining the costs of the users in reality. For example, when transmittingpackets in a communication network, routing traffic in a road network, or processing a task in aproduction system, actual sharing and congestion of resources crucially depends on time.In [13], we introducedtimed network games, which add a time component to network games.Each vertexvin the network is associated with a cost function, mapping the load onvto theprice that a player pays for staying invfor one time unit with this load.  Each edge in thenetwork is guarded by the time intervals in which it can be traversed, which forces the players tospend time in the vertices. In this work we significantly extend the way time can be referred toin timed network games. In the model we study, the network is equipped withclocks, and, as intimed automata, edges are guarded by constraints on the values of the clocks, and their traversalmay involve a reset of some clocks. We argue that the stronger model captures many realisticnetworks.  The addition of clocks breaks the techniques we developed in [13] and we developnew techniques in order to show that positive results on classic network games carry over to thestronger timed setting."}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"day":"01","oa_version":"Published Version","publication_status":"published"},{"abstract":[{"text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally-optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an over-approximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. We extend the abstraction-refinement methodology to labeled networks, where the objectives of the players are regular languages. Our experimental results demonstrate the effectiveness of the methodology. ","lang":"eng"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"day":"01","oa_version":"Published Version","publication_status":"published","date_updated":"2023-09-22T09:48:59Z","status":"public","title":"An abstraction-refinement methodology for reasoning about network games","file":[{"file_size":505155,"file_name":"2018_MDPI_Avni.pdf","date_updated":"2020-07-14T12:47:16Z","checksum":"749d65ca4ce74256a029d9644a1b1cb0","file_id":"6008","date_created":"2019-02-14T14:20:31Z","creator":"kschuh","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1003"}]},"publication":"Games","citation":{"chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>. MDPI AG, 2018. <a href=\"https://doi.org/10.3390/g9030039\">https://doi.org/10.3390/g9030039</a>.","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” <i>Games</i>, vol. 9, no. 3. MDPI AG, 2018.","apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2018). An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. MDPI AG. <a href=\"https://doi.org/10.3390/g9030039\">https://doi.org/10.3390/g9030039</a>","mla":"Avni, Guy, et al. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>, vol. 9, no. 3, 39, MDPI AG, 2018, doi:<a href=\"https://doi.org/10.3390/g9030039\">10.3390/g9030039</a>.","ista":"Avni G, Guha S, Kupferman O. 2018. An abstraction-refinement methodology for reasoning about network games. Games. 9(3), 39.","short":"G. Avni, S. Guha, O. Kupferman, Games 9 (2018).","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. 2018;9(3). doi:<a href=\"https://doi.org/10.3390/g9030039\">10.3390/g9030039</a>"},"project":[{"call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"has_accepted_license":"1","scopus_import":1,"issue":"3","_id":"6006","oa":1,"author":[{"full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"date_published":"2018-09-01T00:00:00Z","year":"2018","publisher":"MDPI AG","doi":"10.3390/g9030039","language":[{"iso":"eng"}],"type":"journal_article","publication_identifier":{"issn":["2073-4336"]},"quality_controlled":"1","month":"09","volume":9,"department":[{"_id":"ToHe"}],"article_number":"39","date_created":"2019-02-14T14:17:54Z","intvolume":"         9","file_date_updated":"2020-07-14T12:47:16Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"]}]