[{"month":"06","publication_identifier":{"isbn":["9781577358800"]},"conference":{"end_date":"2023-02-14","location":"Washington, DC, United States","start_date":"2023-02-07","name":"AAAI: Conference on Artificial Intelligence"},"doi":"10.1609/aaai.v37i5.25679","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1609/aaai.v37i5.25679"}],"external_id":{"arxiv":["2211.13626"]},"oa":1,"quality_controlled":"1","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"ec_funded":1,"author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","first_name":"Ismael R","last_name":"Jecker"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2023-09-05T08:37:00Z","date_created":"2023-08-27T22:01:18Z","volume":37,"year":"2023","acknowledgement":"This research was supported in part by ISF grant no.1679/21, by the ERC CoG 863818 (ForM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"day":"27","article_processing_charge":"No","scopus_import":"1","date_published":"2023-06-27T00:00:00Z","publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","citation":{"ista":"Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471.","apa":"Avni, G., Jecker, I. R., & Zikelic, D. (2023). Bidding graph games with partially-observable budgets. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (Vol. 37, pp. 5464–5471). Washington, DC, United States. https://doi.org/10.1609/aaai.v37i5.25679","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Bidding graph games with partially-observable budgets,” in Proceedings of the 37th AAAI Conference on Artificial Intelligence, Washington, DC, United States, 2023, vol. 37, no. 5, pp. 5464–5471.","ama":"Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Bidding Graph Games with Partially-Observable Budgets.” In Proceedings of the 37th AAAI Conference on Artificial Intelligence, 37:5464–71, 2023. https://doi.org/10.1609/aaai.v37i5.25679.","mla":"Avni, Guy, et al. “Bidding Graph Games with Partially-Observable Budgets.” Proceedings of the 37th AAAI Conference on Artificial Intelligence, vol. 37, no. 5, 2023, pp. 5464–71, doi:10.1609/aaai.v37i5.25679.","short":"G. Avni, I.R. Jecker, D. Zikelic, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, 2023, pp. 5464–5471."},"page":"5464-5471","abstract":[{"text":"Two-player zero-sum \"graph games\" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In \"bidding games\", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with \"mean-payoff\" objectives in combination with \"poorman\" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the \"value\" under pure strategies does not necessarily exist in such games.","lang":"eng"}],"issue":"5","type":"conference","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14243","title":"Bidding graph games with partially-observable budgets","status":"public","intvolume":" 37"},{"citation":{"mla":"Avni, Guy, et al. “Reachability Poorman Discrete-Bidding Games.” Frontiers in Artificial Intelligence and Applications, vol. 372, IOS Press, 2023, pp. 141–48, doi:10.3233/FAIA230264.","short":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, D. Zikelic, in:, Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 141–148.","chicago":"Avni, Guy, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, and Dorde Zikelic. “Reachability Poorman Discrete-Bidding Games.” In Frontiers in Artificial Intelligence and Applications, 372:141–48. IOS Press, 2023. https://doi.org/10.3233/FAIA230264.","ama":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. Reachability poorman discrete-bidding games. In: Frontiers in Artificial Intelligence and Applications. Vol 372. IOS Press; 2023:141-148. doi:10.3233/FAIA230264","ista":"Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications. ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.","apa":"Avni, G., Meggendorfer, T., Sadhukhan, S., Tkadlec, J., & Zikelic, D. (2023). Reachability poorman discrete-bidding games. In Frontiers in Artificial Intelligence and Applications (Vol. 372, pp. 141–148). Krakow, Poland: IOS Press. https://doi.org/10.3233/FAIA230264","ieee":"G. Avni, T. Meggendorfer, S. Sadhukhan, J. Tkadlec, and D. Zikelic, “Reachability poorman discrete-bidding games,” in Frontiers in Artificial Intelligence and Applications, Krakow, Poland, 2023, vol. 372, pp. 141–148."},"publication":"Frontiers in Artificial Intelligence and Applications","page":"141-148","date_published":"2023-09-28T00:00:00Z","scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"28","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"14518","intvolume":" 372","status":"public","ddc":["000"],"title":"Reachability poorman discrete-bidding games","file":[{"creator":"dernst","content_type":"application/pdf","file_size":501011,"file_name":"2023_FAIA_Avni.pdf","access_level":"open_access","date_created":"2023-11-13T10:16:10Z","date_updated":"2023-11-13T10:16:10Z","success":1,"checksum":"1390ca38480fa4cf286b0f1a42e8c12f","file_id":"14529","relation":"main_file"}],"oa_version":"Published Version","type":"conference","abstract":[{"lang":"eng","text":"We consider bidding games, a class of two-player zero-sum graph games. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token, where we break bidding ties in favor of Player 1. Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, poorman discrete-bidding in which the granularity of the bids is restricted and the higher bid is paid to the bank. Previous work either did not impose granularity restrictions or considered Richman bidding (bids are paid to the opponent). While the latter mechanisms are technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on threshold budgets, which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We first show existence of thresholds. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuous-bidding and that they exhibit a periodic behavior. We identify closed-form solutions in special cases. We implement and experiment with an algorithm to find threshold budgets."}],"external_id":{"arxiv":["2307.15218"]},"tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)"},"oa":1,"project":[{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"quality_controlled":"1","doi":"10.3233/FAIA230264","conference":{"name":"ECAI: European Conference on Artificial Intelligence","end_date":"2023-10-04","start_date":"2023-09-30","location":"Krakow, Poland"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0922-6389"],"isbn":["9781643684369"]},"month":"09","acknowledgement":"This research was supported in part by ISF grant no. 1679/21, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie Grant Agreement No. 665385.","year":"2023","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"IOS Press","publication_status":"published","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165"},{"full_name":"Sadhukhan, Suman","last_name":"Sadhukhan","first_name":"Suman"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"volume":372,"date_created":"2023-11-12T23:00:56Z","date_updated":"2023-11-13T10:18:45Z","ec_funded":1,"file_date_updated":"2023-11-13T10:16:10Z","license":"https://creativecommons.org/licenses/by-nc/4.0/"},{"scopus_import":"1","series_title":"Leibniz International Proceedings in Informatics (LIPIcs)","has_accepted_license":"1","article_processing_charge":"No","day":"22","citation":{"ama":"Avni G, Henzinger TA. An updated survey of bidding games on graphs. In: 47th International Symposium on Mathematical Foundations of Computer Science. Vol 241. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:3:1-3:6. doi:10.4230/LIPIcs.MFCS.2022.3","ista":"Avni G, Henzinger TA. 2022. An updated survey of bidding games on graphs. 47th International Symposium on Mathematical Foundations of Computer Science. MFCS: Symposium on Mathematical Foundations of Computer ScienceLeibniz International Proceedings in Informatics (LIPIcs) vol. 241, 3:1-3:6.","ieee":"G. Avni and T. A. Henzinger, “An updated survey of bidding games on graphs,” in 47th International Symposium on Mathematical Foundations of Computer Science, Vienna, Austria, 2022, vol. 241, p. 3:1-3:6.","apa":"Avni, G., & Henzinger, T. A. (2022). An updated survey of bidding games on graphs. In 47th International Symposium on Mathematical Foundations of Computer Science (Vol. 241, p. 3:1-3:6). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.3","mla":"Avni, Guy, and Thomas A. Henzinger. “An Updated Survey of Bidding Games on Graphs.” 47th International Symposium on Mathematical Foundations of Computer Science, vol. 241, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 3:1-3:6, doi:10.4230/LIPIcs.MFCS.2022.3.","short":"G. Avni, T.A. Henzinger, in:, 47th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2022, p. 3:1-3:6.","chicago":"Avni, Guy, and Thomas A Henzinger. “An Updated Survey of Bidding Games on Graphs.” In 47th International Symposium on Mathematical Foundations of Computer Science, 241:3:1-3:6. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.MFCS.2022.3."},"publication":"47th International Symposium on Mathematical Foundations of Computer Science","page":"3:1-3:6","date_published":"2022-08-22T00:00:00Z","type":"conference","abstract":[{"text":"A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an \"auction\" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"12509","intvolume":" 241","ddc":["000"],"status":"public","title":"An updated survey of bidding games on graphs","oa_version":"Published Version","file":[{"date_created":"2023-02-06T09:13:04Z","date_updated":"2023-02-06T09:13:04Z","success":1,"checksum":"1888ec9421622f9526fbec2de035f132","file_id":"12519","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":624586,"file_name":"2022_LIPICs_Avni.pdf","access_level":"open_access"}],"publication_identifier":{"isbn":["9783959772563"],"issn":["1868-8969"]},"month":"08","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.MFCS.2022.3","conference":{"end_date":"2022-08-26","start_date":"2022-08-22","location":"Vienna, Austria","name":"MFCS: Symposium on Mathematical Foundations of Computer Science"},"language":[{"iso":"eng"}],"place":"Dagstuhl, Germany","ec_funded":1,"file_date_updated":"2023-02-06T09:13:04Z","license":"https://creativecommons.org/licenses/by/4.0/","year":"2022","acknowledgement":"Guy Avni: Work partially supported by the Israel Science Foundation, ISF grant agreement\r\nno 1679/21.\r\nThomas A. Henzinger: This work was supported in part by the ERC-2020-AdG 101020093.\r\nWe would like to thank all our collaborators Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný, Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful for you as it was for us.","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","author":[{"last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger"}],"volume":241,"date_created":"2023-02-05T17:26:01Z","date_updated":"2023-02-06T09:16:54Z"},{"page":"617-636","citation":{"short":"G. Avni, I.R. Jecker, D. Zikelic, in:, D. Marx (Ed.), Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial and Applied Mathematics, 2021, pp. 617–636.","mla":"Avni, Guy, et al. “Infinite-Duration All-Pay Bidding Games.” Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, edited by Dániel Marx, Society for Industrial and Applied Mathematics, 2021, pp. 617–36, doi:10.1137/1.9781611976465.38.","chicago":"Avni, Guy, Ismael R Jecker, and Dorde Zikelic. “Infinite-Duration All-Pay Bidding Games.” In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, edited by Dániel Marx, 617–36. Society for Industrial and Applied Mathematics, 2021. https://doi.org/10.1137/1.9781611976465.38.","ama":"Avni G, Jecker IR, Zikelic D. Infinite-duration all-pay bidding games. In: Marx D, ed. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms. Society for Industrial and Applied Mathematics; 2021:617-636. doi:10.1137/1.9781611976465.38","apa":"Avni, G., Jecker, I. R., & Zikelic, D. (2021). Infinite-duration all-pay bidding games. In D. Marx (Ed.), Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (pp. 617–636). Virtual: Society for Industrial and Applied Mathematics. https://doi.org/10.1137/1.9781611976465.38","ieee":"G. Avni, I. R. Jecker, and D. Zikelic, “Infinite-duration all-pay bidding games,” in Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, Virtual, 2021, pp. 617–636.","ista":"Avni G, Jecker IR, Zikelic D. 2021. Infinite-duration all-pay bidding games. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 617–636."},"publication":"Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms","date_published":"2021-01-01T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"01","status":"public","title":"Infinite-duration all-pay bidding games","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"10694","oa_version":"Preprint","type":"conference","abstract":[{"text":"In a two-player zero-sum graph game the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In bidding games, however, the players have budgets, and in each turn, we hold an “auction” (bidding) to determine which player moves the token: both players simultaneously submit bids and the higher bidder moves the token. The bidding mechanisms differ in their payment schemes. Bidding games were largely studied with variants of first-price bidding in which only the higher bidder pays his bid. We focus on all-pay bidding, where both players pay their bids. Finite-duration all-pay bidding games were studied and shown to be technically more challenging than their first-price counterparts. We study for the first time, infinite-duration all-pay bidding games. Our most interesting results are for mean-payoff objectives: we portray a complete picture for games played on strongly-connected graphs. We study both pure (deterministic) and mixed (probabilistic) strategies and completely characterize the optimal and almost-sure (with probability 1) payoffs the players can respectively guarantee. We show that mean-payoff games under all-pay bidding exhibit the intriguing mathematical properties of their first-price counterparts; namely, an equivalence with random-turn games in which in each turn, the player who moves is selected according to a (biased) coin toss. The equivalences for all-pay bidding are more intricate and unexpected than for first-price bidding.","lang":"eng"}],"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"call_identifier":"H2020","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"quality_controlled":"1","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2005.06636"}],"external_id":{"arxiv":["2005.06636"]},"language":[{"iso":"eng"}],"doi":"10.1137/1.9781611976465.38","conference":{"location":"Virtual","start_date":"2021-01-10","end_date":"2021-01-13","name":"SODA: Symposium on Discrete Algorithms"},"publication_identifier":{"isbn":["978-1-61197-646-5"]},"month":"01","publisher":"Society for Industrial and Applied Mathematics","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"editor":[{"full_name":"Marx, Dániel","last_name":"Marx","first_name":"Dániel"}],"publication_status":"published","year":"2021","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and by the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","date_created":"2022-01-27T12:11:23Z","date_updated":"2022-01-27T12:58:43Z","author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni"},{"full_name":"Jecker, Ismael R","id":"85D7C63E-7D5D-11E9-9C0F-98C4E5697425","first_name":"Ismael R","last_name":"Jecker"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","full_name":"Zikelic, Dorde"}],"ec_funded":1},{"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Elsevier","year":"2021","date_updated":"2023-08-07T14:08:34Z","date_created":"2021-03-14T23:01:32Z","volume":119,"author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"last_name":"Žikelić","first_name":"Đorđe","full_name":"Žikelić, Đorđe"}],"related_material":{"record":[{"id":"6884","status":"public","relation":"earlier_version"}]},"month":"03","publication_identifier":{"eissn":["1090-2724"],"issn":["0022-0000"]},"isi":1,"quality_controlled":"1","external_id":{"arxiv":["1905.03835"],"isi":["000634149800009"]},"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.1905.03835","open_access":"1"}],"oa":1,"language":[{"iso":"eng"}],"doi":"10.1016/j.jcss.2021.02.008","type":"journal_article","abstract":[{"lang":"eng","text":"A graph game proceeds as follows: two players move a token through a graph to produce a finite or infinite path, which determines the payoff of the game. We study bidding games in which in each turn, an auction determines which player moves the token. Bidding games were largely studied in combination with two variants of first-price auctions called “Richman” and “poorman” bidding. We study taxman bidding, which span the spectrum between the two. The game is parameterized by a constant : portion τ of the winning bid is paid to the other player, and portion 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: we unify, generalize, and simplify previous equivalences between bidding games and a class of stochastic games called random-turn games."}],"issue":"8","status":"public","title":"Bidding mechanisms in graph games","intvolume":" 119","_id":"9239","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","scopus_import":"1","day":"03","article_processing_charge":"No","article_type":"original","page":"133-144","publication":"Journal of Computer and System Sciences","citation":{"ama":"Avni G, Henzinger TA, Žikelić Đ. Bidding mechanisms in graph games. Journal of Computer and System Sciences. 2021;119(8):133-144. doi:10.1016/j.jcss.2021.02.008","ista":"Avni G, Henzinger TA, Žikelić Đ. 2021. Bidding mechanisms in graph games. Journal of Computer and System Sciences. 119(8), 133–144.","apa":"Avni, G., Henzinger, T. A., & Žikelić, Đ. (2021). Bidding mechanisms in graph games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2021.02.008","ieee":"G. Avni, T. A. Henzinger, and Đ. Žikelić, “Bidding mechanisms in graph games,” Journal of Computer and System Sciences, vol. 119, no. 8. Elsevier, pp. 133–144, 2021.","mla":"Avni, Guy, et al. “Bidding Mechanisms in Graph Games.” Journal of Computer and System Sciences, vol. 119, no. 8, Elsevier, 2021, pp. 133–44, doi:10.1016/j.jcss.2021.02.008.","short":"G. Avni, T.A. Henzinger, Đ. Žikelić, Journal of Computer and System Sciences 119 (2021) 133–144.","chicago":"Avni, Guy, Thomas A Henzinger, and Đorđe Žikelić. “Bidding Mechanisms in Graph Games.” Journal of Computer and System Sciences. Elsevier, 2021. https://doi.org/10.1016/j.jcss.2021.02.008."},"date_published":"2021-03-03T00:00:00Z"},{"keyword":["computer science","computer science and game theory","logic in computer science"],"scopus_import":"1","day":"03","has_accepted_license":"1","article_processing_charge":"No","article_type":"original","page":"10:1-10:23","publication":"Logical Methods in Computer Science","citation":{"ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. 2021;17(1):10:1-10:23. doi:10.23638/LMCS-17(1:10)2021","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.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” Logical Methods in Computer Science, vol. 17, no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.","apa":"Aghajohari, M., Avni, G., & Henzinger, T. A. (2021). Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. International Federation for Computational Logic. https://doi.org/10.23638/LMCS-17(1:10)2021","mla":"Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration Games.” Logical Methods in Computer Science, vol. 17, no. 1, International Federation for Computational Logic, 2021, p. 10:1-10:23, doi:10.23638/LMCS-17(1:10)2021.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games.” Logical Methods in Computer Science. International Federation for Computational Logic, 2021. https://doi.org/10.23638/LMCS-17(1:10)2021."},"date_published":"2021-02-03T00:00:00Z","type":"journal_article","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 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.","lang":"eng"}],"issue":"1","title":"Determinacy in discrete-bidding infinite-duration games","status":"public","ddc":["510"],"intvolume":" 17","_id":"10674","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"checksum":"b35586a50ed1ca8f44767de116d18d81","success":1,"date_created":"2022-01-26T08:04:50Z","date_updated":"2022-01-26T08:04:50Z","relation":"main_file","file_id":"10690","content_type":"application/pdf","file_size":819878,"creator":"alisjak","access_level":"open_access","file_name":"2021_LMCS_AGHAJOHAR.pdf"}],"oa_version":"Published Version","month":"02","publication_identifier":{"eissn":["1860-5974"]},"isi":1,"quality_controlled":"1","project":[{"name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000658724600010"],"arxiv":["1905.03588"]},"language":[{"iso":"eng"}],"doi":"10.23638/LMCS-17(1:10)2021","file_date_updated":"2022-01-26T08:04:50Z","publication_status":"published","publisher":"International Federation for Computational Logic","department":[{"_id":"ToHe"}],"year":"2021","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_updated":"2023-08-17T06:56:42Z","date_created":"2022-01-25T16:32:13Z","volume":17,"author":[{"full_name":"Aghajohari, Milad","first_name":"Milad","last_name":"Aghajohari"},{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}]},{"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"quality_controlled":"1","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CONCUR.2020.2","conference":{"end_date":"2020-09-04","location":"Virtual","start_date":"2020-09-01","name":"CONCUR: Conference on Concurrency Theory"},"publication_identifier":{"isbn":["9783959771603"],"issn":["18688969"]},"month":"08","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","acknowledgement":"We would like to thank all our collaborators Milad Aghajohari, Ventsislav Chonev, Rasmus Ibsen-Jensen, Ismäel Jecker, Petr Novotný, Josef Tkadlec, and Ðorđe Žikelić; we hope the collaboration was as fun and meaningful for you as it was for us.","volume":171,"date_updated":"2021-01-12T08:20:13Z","date_created":"2020-10-04T22:01:36Z","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"article_number":"2","license":"https://creativecommons.org/licenses/by/3.0/","file_date_updated":"2020-10-05T14:13:19Z","citation":{"ista":"Avni G, Henzinger TA. 2020. A survey of bidding games on graphs. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 2.","ieee":"G. Avni and T. A. Henzinger, “A survey of bidding games on graphs,” in 31st International Conference on Concurrency Theory, Virtual, 2020, vol. 171.","apa":"Avni, G., & Henzinger, T. A. (2020). A survey of bidding games on graphs. In 31st International Conference on Concurrency Theory (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2","ama":"Avni G, Henzinger TA. A survey of bidding games on graphs. In: 31st International Conference on Concurrency Theory. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CONCUR.2020.2","chicago":"Avni, Guy, and Thomas A Henzinger. “A Survey of Bidding Games on Graphs.” In 31st International Conference on Concurrency Theory, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.2.","mla":"Avni, Guy, and Thomas A. Henzinger. “A Survey of Bidding Games on Graphs.” 31st International Conference on Concurrency Theory, vol. 171, 2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CONCUR.2020.2.","short":"G. Avni, T.A. Henzinger, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020."},"publication":"31st International Conference on Concurrency Theory","date_published":"2020-08-06T00:00:00Z","scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"06","intvolume":" 171","ddc":["000"],"title":"A survey of bidding games on graphs","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"8599","oa_version":"Published Version","file":[{"date_created":"2020-10-05T14:13:19Z","date_updated":"2020-10-05T14:13:19Z","checksum":"8f33b098e73724e0ac817f764d8e1a2d","success":1,"relation":"main_file","file_id":"8611","file_size":868510,"content_type":"application/pdf","creator":"dernst","file_name":"2020_LIPIcsCONCUR_Avni.pdf","access_level":"open_access"}],"alternative_title":["LIPIcs"],"type":"conference","abstract":[{"lang":"eng","text":"A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an \"auction\" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games."}]},{"abstract":[{"lang":"eng","text":"Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the wizard, we extract from it a decision-tree based model, which we refer to as the magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, a synthesis procedure that is based on a magic book. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training."}],"type":"conference","file":[{"relation":"main_file","file_id":"9109","date_created":"2021-02-09T09:39:02Z","date_updated":"2021-02-09T09:39:02Z","checksum":"d616d549a0ade78606b16f8a9540820f","success":1,"file_name":"2020_FMCAD_Alamdari.pdf","access_level":"open_access","content_type":"application/pdf","file_size":990999,"creator":"dernst"}],"oa_version":"Published Version","_id":"9040","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Formal methods with a touch of magic","ddc":["000"],"article_processing_charge":"No","has_accepted_license":"1","day":"21","scopus_import":"1","date_published":"2020-09-21T00:00:00Z","citation":{"ama":"Alamdari PA, Avni G, Henzinger TA, Lukina A. Formal methods with a touch of magic. In: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design. TU Wien Academic Press; 2020:138-147. doi:10.34727/2020/isbn.978-3-85448-042-6_21","ista":"Alamdari PA, Avni G, Henzinger TA, Lukina A. 2020. Formal methods with a touch of magic. Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 138–147.","apa":"Alamdari, P. A., Avni, G., Henzinger, T. A., & Lukina, A. (2020). Formal methods with a touch of magic. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (pp. 138–147). Online Conference: TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21","ieee":"P. A. Alamdari, G. Avni, T. A. Henzinger, and A. Lukina, “Formal methods with a touch of magic,” in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, Online Conference, 2020, pp. 138–147.","mla":"Alamdari, Par Alizadeh, et al. “Formal Methods with a Touch of Magic.” Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2020, pp. 138–47, doi:10.34727/2020/isbn.978-3-85448-042-6_21.","short":"P.A. Alamdari, G. Avni, T.A. Henzinger, A. Lukina, in:, Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2020, pp. 138–147.","chicago":"Alamdari, Par Alizadeh, Guy Avni, Thomas A Henzinger, and Anna Lukina. “Formal Methods with a Touch of Magic.” In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, 138–47. TU Wien Academic Press, 2020. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21."},"publication":"Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design","page":"138-147","file_date_updated":"2021-02-09T09:39:02Z","author":[{"last_name":"Alamdari","first_name":"Par Alizadeh","full_name":"Alamdari, Par Alizadeh"},{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"full_name":"Lukina, Anna","last_name":"Lukina","first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"}],"date_updated":"2021-02-09T09:39:59Z","date_created":"2021-01-24T23:01:10Z","year":"2020","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"publisher":"TU Wien Academic Press","publication_status":"published","publication_identifier":{"eissn":["2708-7824"],"isbn":["9783854480426"]},"month":"09","doi":"10.34727/2020/isbn.978-3-85448-042-6_21","conference":{"name":" FMCAD: Formal Methods in Computer-Aided Design","end_date":"2020-09-24","start_date":"2020-09-21","location":"Online Conference"},"language":[{"iso":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1"},{"isi":1,"quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"}],"oa":1,"external_id":{"isi":["000512219400004"]},"language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2019.06.031","month":"02","publication_identifier":{"issn":["03043975"]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Elsevier","year":"2020","date_updated":"2023-08-17T13:52:49Z","date_created":"2019-08-04T21:59:20Z","volume":807,"author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"related_material":{"record":[{"id":"1341","relation":"earlier_version","status":"public"}]},"file_date_updated":"2020-10-09T06:31:22Z","article_type":"original","page":"42-55","publication":"Theoretical Computer Science","citation":{"ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. Theoretical Computer Science. 2020;807:42-55. doi:10.1016/j.tcs.2019.06.031","ista":"Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games. Theoretical Computer Science. 807, 42–55.","apa":"Avni, G., Henzinger, T. A., & Kupferman, O. (2020). Dynamic resource allocation games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2019.06.031","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” Theoretical Computer Science, vol. 807. Elsevier, pp. 42–55, 2020.","mla":"Avni, Guy, et al. “Dynamic Resource Allocation Games.” Theoretical Computer Science, vol. 807, Elsevier, 2020, pp. 42–55, doi:10.1016/j.tcs.2019.06.031.","short":"G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020) 42–55.","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games.” Theoretical Computer Science. Elsevier, 2020. https://doi.org/10.1016/j.tcs.2019.06.031."},"date_published":"2020-02-06T00:00:00Z","scopus_import":"1","day":"06","article_processing_charge":"No","has_accepted_license":"1","ddc":["000"],"title":"Dynamic resource allocation games","status":"public","intvolume":" 807","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6761","oa_version":"Submitted Version","file":[{"success":1,"checksum":"e86635417f45eb2cd75778f91382f737","date_created":"2020-10-09T06:31:22Z","date_updated":"2020-10-09T06:31:22Z","file_id":"8639","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":1413001,"access_level":"open_access","file_name":"2020_TheoreticalCS_Avni.pdf"}],"type":"journal_article","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."}]},{"date_published":"2020-04-03T00:00:00Z","article_type":"original","page":"1798-1805","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","citation":{"ama":"Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. 2020;34(02):1798-1805. doi:10.1609/aaai.v34i02.5546","apa":"Avni, G., Ibsen-Jensen, R., & Tkadlec, J. (2020). All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. New York, NY, United States: Association for the Advancement of Artificial Intelligence. https://doi.org/10.1609/aaai.v34i02.5546","ieee":"G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805, 2020.","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.","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.” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 02, Association for the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:10.1609/aaai.v34i02.5546.","chicago":"Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games on Graphs.” Proceedings of the AAAI Conference on Artificial Intelligence. Association for the Advancement of Artificial Intelligence, 2020. https://doi.org/10.1609/aaai.v34i02.5546."},"day":"03","article_processing_charge":"No","scopus_import":"1","oa_version":"Preprint","title":"All-pay bidding games on graphs","status":"public","intvolume":" 34","_id":"9197","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","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."}],"issue":"02","type":"journal_article","language":[{"iso":"eng"}],"conference":{"name":"AAAI: Conference on Artificial Intelligence","location":"New York, NY, United States","start_date":"2020-02-07","end_date":"2020-02-12"},"doi":"10.1609/aaai.v34i02.5546","quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"}],"external_id":{"arxiv":["1911.08360"]},"month":"04","publication_identifier":{"issn":["2159-5399"],"isbn":["9781577358350"],"eissn":["2374-3468"]},"date_updated":"2023-09-05T12:40:00Z","date_created":"2021-02-25T09:05:18Z","volume":34,"author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Tkadlec","first_name":"Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef"}],"publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","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).","year":"2020"},{"scopus_import":1,"day":"06","has_accepted_license":"1","publication":" Proceedings of the 13th International Conference of Reachability Problems","citation":{"apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., & Novotny, P. (2019). Bidding games on Markov decision processes. In Proceedings of the 13th International Conference of Reachability Problems (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. https://doi.org/10.1007/978-3-030-30806-3_1","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in Proceedings of the 13th International Conference of Reachability Problems, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","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.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: Proceedings of the 13th International Conference of Reachability Problems. Vol 11674. Springer; 2019:1-12. doi:10.1007/978-3-030-30806-3_1","chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In Proceedings of the 13th International Conference of Reachability Problems, 11674:1–12. Springer, 2019. https://doi.org/10.1007/978-3-030-30806-3_1.","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.","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” Proceedings of the 13th International Conference of Reachability Problems, vol. 11674, Springer, 2019, pp. 1–12, doi:10.1007/978-3-030-30806-3_1."},"page":"1-12","date_published":"2019-09-06T00:00:00Z","type":"conference","alternative_title":["LNCS"],"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"}],"_id":"6822","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"status":"public","title":"Bidding games on Markov decision processes","intvolume":" 11674","file":[{"creator":"gavni","file_size":436635,"content_type":"application/pdf","file_name":"prob.pdf","access_level":"open_access","date_created":"2019-08-19T07:56:40Z","date_updated":"2020-07-14T12:47:41Z","checksum":"45ebbc709af2b247d28c7c293c01504b","file_id":"6823","relation":"main_file"}],"oa_version":"Submitted Version","month":"09","publication_identifier":{"isbn":["978-303030805-6"],"issn":["0302-9743"]},"oa":1,"quality_controlled":"1","project":[{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"RP: Reachability Problems","end_date":"2019-09-13","location":"Brussels, Belgium","start_date":"2019-09-11"},"doi":"10.1007/978-3-030-30806-3_1","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:47:41Z","year":"2019","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny"}],"date_created":"2019-08-19T07:58:10Z","date_updated":"2021-01-12T08:09:12Z","volume":11674},{"article_processing_charge":"No","has_accepted_license":"1","day":"01","scopus_import":"1","date_published":"2019-08-01T00:00:00Z","citation":{"mla":"Aghajohari, Milad, et al. Determinacy in Discrete-Bidding Infinite-Duration Games. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.CONCUR.2019.20.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","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. https://doi.org/10.4230/LIPICS.CONCUR.2019.20.","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:10.4230/LIPICS.CONCUR.2019.20","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., & 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. https://doi.org/10.4230/LIPICS.CONCUR.2019.20","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."},"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. "}],"type":"conference","alternative_title":["LIPIcs"],"oa_version":"Published Version","file":[{"file_id":"6915","relation":"main_file","date_updated":"2020-07-14T12:47:43Z","date_created":"2019-09-27T12:21:38Z","checksum":"4df6d3575c506edb17215adada03cc8e","file_name":"2019_LIPIcs_Aghajohari.pdf","access_level":"open_access","creator":"kschuh","file_size":741425,"content_type":"application/pdf"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"6886","intvolume":" 140","ddc":["000"],"title":"Determinacy in discrete-bidding infinite-duration games","status":"public","month":"08","doi":"10.4230/LIPICS.CONCUR.2019.20","conference":{"name":"CONCUR: International Conference on Concurrency Theory","end_date":"2019-08-30","start_date":"2019-08-27","location":"Amsterdam, Netherlands"},"language":[{"iso":"eng"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["1905.03588"]},"oa":1,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:43Z","article_number":"20","author":[{"first_name":"Milad","last_name":"Aghajohari","full_name":"Aghajohari, Milad"},{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"volume":140,"date_created":"2019-09-18T08:06:58Z","date_updated":"2022-01-26T08:27:10Z","year":"2019","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published"},{"file":[{"access_level":"open_access","file_name":"2019_LIPIcs_Avni.pdf","file_size":554457,"content_type":"application/pdf","creator":"kschuh","relation":"main_file","file_id":"6913","checksum":"6346e116a4f4ed1414174d96d2c4fbd7","date_created":"2019-09-27T11:45:15Z","date_updated":"2020-07-14T12:47:42Z"}],"oa_version":"Published Version","title":"Bidding mechanisms in graph games","status":"public","ddc":["004"],"intvolume":" 138","_id":"6884","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","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. "}],"alternative_title":["LIPIcs"],"type":"conference","date_published":"2019-08-01T00:00:00Z","citation":{"mla":"Avni, Guy, et al. Bidding Mechanisms in Graph Games. Vol. 138, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.MFCS.2019.11.","short":"G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","chicago":"Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. https://doi.org/10.4230/LIPICS.MFCS.2019.11.","ama":"Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.MFCS.2019.11","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.","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.","apa":"Avni, G., Henzinger, T. A., & 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. https://doi.org/10.4230/LIPICS.MFCS.2019.11"},"day":"01","has_accepted_license":"1","scopus_import":1,"date_created":"2019-09-18T08:04:26Z","date_updated":"2023-08-07T14:08:34Z","volume":138,"author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"9239","relation":"later_version","status":"public"}]},"publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2019","file_date_updated":"2020-07-14T12:47:42Z","ec_funded":1,"article_number":"11","language":[{"iso":"eng"}],"conference":{"end_date":"2019-08-30","start_date":"2019-08-26","location":"Aachen, Germany","name":"MFCS: nternational Symposium on Mathematical Foundations of Computer Science"},"doi":"10.4230/LIPICS.MFCS.2019.11","quality_controlled":"1","project":[{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"},{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["1905.03835"]},"month":"08"},{"publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]},"month":"07","project":[{"grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"quality_controlled":"1","isi":1,"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000491468000036"]},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-030-25540-4_36","conference":{"name":"CAV: Computer Aided Verification","start_date":"2019-07-13","location":"New York, NY, United States","end_date":"2019-07-18"},"file_date_updated":"2020-07-14T12:47:31Z","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publication_status":"published","year":"2019","volume":11561,"date_updated":"2023-08-25T10:33:27Z","date_created":"2019-05-16T11:22:30Z","author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"first_name":"Roderick","last_name":"Bloem","full_name":"Bloem, Roderick"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Konighofer, Bettina","last_name":"Konighofer","first_name":"Bettina"},{"full_name":"Pranger, Stefan","last_name":"Pranger","first_name":"Stefan"}],"scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"12","page":"630-649","citation":{"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 31st International Conference on Computer-Aided Verification, New York, NY, United States, 2019, vol. 11561, pp. 630–649.","apa":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., & Pranger, S. (2019). Run-time optimization for learned controllers through quantitative games. In 31st International Conference on Computer-Aided Verification (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. https://doi.org/10.1007/978-3-030-25540-4_36","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: 31st International Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:630-649. doi:10.1007/978-3-030-25540-4_36","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 31st International Conference on Computer-Aided Verification, 11561:630–49. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_36.","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.” 31st International Conference on Computer-Aided Verification, vol. 11561, Springer, 2019, pp. 630–49, doi:10.1007/978-3-030-25540-4_36."},"publication":"31st International Conference on Computer-Aided Verification","date_published":"2019-07-12T00:00:00Z","alternative_title":["LNCS"],"type":"conference","abstract":[{"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.","lang":"eng"}],"intvolume":" 11561","status":"public","ddc":["000"],"title":"Run-time optimization for learned controllers through quantitative games","_id":"6462","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Published Version","file":[{"access_level":"open_access","file_name":"2019_CAV_Avni.pdf","file_size":659766,"content_type":"application/pdf","creator":"dernst","relation":"main_file","file_id":"6816","checksum":"c231579f2485c6fd4df17c9443a4d80b","date_updated":"2020-07-14T12:47:31Z","date_created":"2019-08-14T09:35:24Z"}]},{"oa_version":"Preprint","title":"Infinite-duration bidding games","status":"public","intvolume":" 66","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6752","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."}],"issue":"4","type":"journal_article","date_published":"2019-07-16T00:00:00Z","publication":"Journal of the ACM","citation":{"chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3340295.","mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM, vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295.","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.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” Journal of the ACM, vol. 66, no. 4. ACM, 2019.","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2019). Infinite-duration bidding games. Journal of the ACM. ACM. https://doi.org/10.1145/3340295","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal of the ACM. 2019;66(4). doi:10.1145/3340295"},"day":"16","article_processing_charge":"No","scopus_import":"1","date_created":"2019-08-04T21:59:16Z","date_updated":"2023-08-29T07:02:13Z","volume":66,"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"950","relation":"earlier_version","status":"public"}]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"ACM","year":"2019","article_number":"31","language":[{"iso":"eng"}],"doi":"10.1145/3340295","quality_controlled":"1","isi":1,"project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"}],"external_id":{"isi":["000487714900008"],"arxiv":["1705.01433"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.01433"}],"oa":1,"month":"07","publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]}},{"article_number":"23","file_date_updated":"2020-07-14T12:47:15Z","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2018","date_updated":"2023-02-23T14:02:58Z","date_created":"2019-02-14T14:12:09Z","volume":117,"author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"963"}]},"month":"08","publication_identifier":{"issn":["1868-8969"]},"quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"language":[{"iso":"eng"}],"conference":{"end_date":"2018-08-31","start_date":"2018-08-27","location":"Liverpool, United Kingdom","name":"MFCS: Mathematical Foundations of Computer Science"},"doi":"10.4230/LIPICS.MFCS.2018.23","alternative_title":["LIPIcs"],"type":"conference","abstract":[{"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.","lang":"eng"}],"status":"public","title":"Timed network games with clocks","ddc":["000"],"intvolume":" 117","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"6005","oa_version":"Published Version","file":[{"creator":"dernst","content_type":"application/pdf","file_size":542889,"file_name":"2018_LIPIcs_Avni.pdf","access_level":"open_access","date_created":"2019-02-14T14:22:04Z","date_updated":"2020-07-14T12:47:15Z","checksum":"41ab2ae9b63f5eb49fa995250c0ba128","file_id":"6007","relation":"main_file"}],"scopus_import":"1","day":"01","article_processing_charge":"No","has_accepted_license":"1","citation":{"mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 117, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPICS.MFCS.2018.23.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPICS.MFCS.2018.23.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPICS.MFCS.2018.23","ista":"Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23.","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.","apa":"Avni, G., Guha, S., & 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. https://doi.org/10.4230/LIPICS.MFCS.2018.23"},"date_published":"2018-08-01T00:00:00Z"},{"oa_version":"Preprint","_id":"5788","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Infinite-duration poorman-bidding games","status":"public","intvolume":" 11316","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 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."}],"type":"conference","alternative_title":["LNCS"],"date_published":"2018-11-21T00:00:00Z","citation":{"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.","apa":"Avni, G., Henzinger, T. A., & 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. https://doi.org/10.1007/978-3-030-04612-5_2","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.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R. Infinite-duration poorman-bidding games. In: Vol 11316. Springer; 2018:21-36. doi:10.1007/978-3-030-04612-5_2","chicago":"Avni, Guy, Thomas A Henzinger, and Rasmus Ibsen-Jensen. “Infinite-Duration Poorman-Bidding Games,” 11316:21–36. Springer, 2018. https://doi.org/10.1007/978-3-030-04612-5_2.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.","mla":"Avni, Guy, et al. Infinite-Duration Poorman-Bidding Games. Vol. 11316, Springer, 2018, pp. 21–36, doi:10.1007/978-3-030-04612-5_2."},"page":"21-36","day":"21","article_processing_charge":"No","scopus_import":"1","author":[{"full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus"}],"date_created":"2018-12-30T22:59:14Z","date_updated":"2023-09-12T07:44:01Z","volume":11316,"year":"2018","publisher":"Springer","department":[{"_id":"ToHe"}],"conference":{"name":"14th International Conference on Web and Internet Economics, WINE","start_date":"2018-12-15","location":"Oxford, UK","end_date":"2018-12-17"},"doi":"10.1007/978-3-030-04612-5_2","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.04372"}],"external_id":{"arxiv":["1804.04372"],"isi":["000865933000002"]},"oa":1,"quality_controlled":"1","isi":1,"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","grant_number":"M02369"}],"month":"11","publication_identifier":{"issn":["03029743"],"isbn":["9783030046118"]}},{"doi":"10.1016/j.tcs.2017.11.001","language":[{"iso":"eng"}],"external_id":{"isi":["000424959200003"]},"main_file_link":[{"open_access":"1","url":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.636.4529"}],"oa":1,"quality_controlled":"1","isi":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"month":"02","author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"date_updated":"2023-09-19T10:00:21Z","date_created":"2018-12-11T11:47:28Z","volume":712,"year":"2018","publication_status":"published","publisher":"Elsevier","department":[{"_id":"ToHe"}],"ec_funded":1,"publist_id":"7197","date_published":"2018-02-15T00:00:00Z","publication":"Theoretical Computer Science","citation":{"mla":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” Theoretical Computer Science, vol. 712, Elsevier, 2018, pp. 50–72, doi:10.1016/j.tcs.2017.11.001.","short":"G. Avni, O. Kupferman, Theoretical Computer Science 712 (2018) 50–72.","chicago":"Avni, Guy, and Orna Kupferman. “Synthesis from Component Libraries with Costs.” Theoretical Computer Science. Elsevier, 2018. https://doi.org/10.1016/j.tcs.2017.11.001.","ama":"Avni G, Kupferman O. Synthesis from component libraries with costs. Theoretical Computer Science. 2018;712:50-72. doi:10.1016/j.tcs.2017.11.001","ista":"Avni G, Kupferman O. 2018. Synthesis from component libraries with costs. Theoretical Computer Science. 712, 50–72.","apa":"Avni, G., & Kupferman, O. (2018). Synthesis from component libraries with costs. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2017.11.001","ieee":"G. Avni and O. Kupferman, “Synthesis from component libraries with costs,” Theoretical Computer Science, vol. 712. Elsevier, pp. 50–72, 2018."},"article_type":"original","page":"50 - 72","day":"15","article_processing_charge":"No","scopus_import":"1","oa_version":"Published Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"608","status":"public","title":"Synthesis from component libraries with costs","intvolume":" 712","abstract":[{"text":"Synthesis is the automated construction of a system from its specification. In real life, hardware and software systems are rarely constructed from scratch. Rather, a system is typically constructed from a library of components. Lustig and Vardi formalized this intuition and studied LTL synthesis from component libraries. In real life, designers seek optimal systems. In this paper we add optimality considerations to the setting. We distinguish between quality considerations (for example, size - the smaller a system is, the better it is), and pricing (for example, the payment to the company who manufactured the component). We study the problem of designing systems with minimal quality-cost and price. A key point is that while the quality cost is individual - the choices of a designer are independent of choices made by other designers that use the same library, pricing gives rise to a resource-allocation game - designers that use the same component share its price, with the share being proportional to the number of uses (a component can be used several times in a design). We study both closed and open settings, and in both we solve the problem of finding an optimal design. In a setting with multiple designers, we also study the game-theoretic problems of the induced resource-allocation game.","lang":"eng"}],"type":"journal_article"},{"scopus_import":1,"has_accepted_license":"1","day":"01","citation":{"short":"G. Avni, S. Guha, O. Kupferman, Games 9 (2018).","mla":"Avni, Guy, et al. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” Games, vol. 9, no. 3, 39, MDPI AG, 2018, doi:10.3390/g9030039.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” Games. MDPI AG, 2018. https://doi.org/10.3390/g9030039.","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. Games. 2018;9(3). doi:10.3390/g9030039","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” Games, vol. 9, no. 3. MDPI AG, 2018.","apa":"Avni, G., Guha, S., & Kupferman, O. (2018). An abstraction-refinement methodology for reasoning about network games. Games. MDPI AG. https://doi.org/10.3390/g9030039","ista":"Avni G, Guha S, Kupferman O. 2018. An abstraction-refinement methodology for reasoning about network games. Games. 9(3), 39."},"publication":"Games","date_published":"2018-09-01T00:00:00Z","type":"journal_article","issue":"3","abstract":[{"lang":"eng","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. "}],"intvolume":" 9","ddc":["004"],"status":"public","title":"An abstraction-refinement methodology for reasoning about network games","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"6006","oa_version":"Published Version","file":[{"file_name":"2018_MDPI_Avni.pdf","access_level":"open_access","content_type":"application/pdf","file_size":505155,"creator":"kschuh","relation":"main_file","file_id":"6008","date_created":"2019-02-14T14:20:31Z","date_updated":"2020-07-14T12:47:16Z","checksum":"749d65ca4ce74256a029d9644a1b1cb0"}],"publication_identifier":{"issn":["2073-4336"]},"month":"09","project":[{"grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.3390/g9030039","article_number":"39","file_date_updated":"2020-07-14T12:47:16Z","publisher":"MDPI AG","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2018","volume":9,"date_created":"2019-02-14T14:17:54Z","date_updated":"2023-09-22T09:48:59Z","related_material":{"record":[{"id":"1003","status":"public","relation":"earlier_version"}]},"author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}]},{"day":"01","has_accepted_license":"1","scopus_import":1,"date_published":"2017-06-01T00:00:00Z","citation":{"chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.37.","mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 83, 37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.37.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 37.","apa":"Avni, G., Guha, S., & Kupferman, O. (2017). Timed network games with clocks (Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.37","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark, 2017, vol. 83.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.37"},"abstract":[{"text":"Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games , which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed. ","lang":"eng"}],"alternative_title":["LIPIcs"],"type":"conference","file":[{"file_id":"5059","relation":"main_file","checksum":"f55eaf7f3c36ea07801112acfedd17d5","date_updated":"2020-07-14T12:48:18Z","date_created":"2018-12-12T10:14:10Z","access_level":"open_access","file_name":"IST-2017-829-v1+1_mfcs-cr.pdf","creator":"system","file_size":369730,"content_type":"application/pdf"}],"oa_version":"Published Version","pubrep_id":"829","title":"Timed network games with clocks","ddc":["004"],"status":"public","intvolume":" 83","_id":"963","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06","publication_identifier":{"issn":["18688969"]},"language":[{"iso":"eng"}],"conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","location":"Aalborg, Denmark","start_date":"2017-08-21","end_date":"2017-08-25"},"doi":"10.4230/LIPIcs.MFCS.2017.37","quality_controlled":"1","project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"file_date_updated":"2020-07-14T12:48:18Z","publist_id":"6438","article_number":"37","date_created":"2018-12-11T11:49:26Z","date_updated":"2023-02-23T12:35:50Z","volume":83,"author":[{"full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"related_material":{"record":[{"id":"6005","status":"public","relation":"later_version"}]},"publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"year":"2017"},{"month":"09","publication_identifier":{"issn":["1868-8969"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["1705.01433"]},"quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"CONCUR: Concurrency Theory","location":"Berlin, Germany","start_date":"2017-09-05","end_date":"2017-09-07"},"doi":"10.4230/LIPIcs.CONCUR.2017.21","language":[{"iso":"eng"}],"article_number":"17","file_date_updated":"2020-07-14T12:48:16Z","publist_id":"6466","year":"2017","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","last_name":"Chonev","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"6752"}]},"date_updated":"2023-08-29T07:02:13Z","date_created":"2018-12-11T11:49:22Z","volume":85,"scopus_import":1,"day":"01","has_accepted_license":"1","citation":{"mla":"Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85."},"date_published":"2017-09-01T00:00:00Z","type":"conference","alternative_title":["LIPIcs"],"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. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"950","status":"public","title":"Infinite-duration bidding games","ddc":["000"],"intvolume":" 85","pubrep_id":"844","oa_version":"Published Version","file":[{"file_id":"5318","relation":"main_file","date_updated":"2020-07-14T12:48:16Z","date_created":"2018-12-12T10:18:00Z","checksum":"6d5cccf755207b91ccbef95d8275b013","file_name":"IST-2017-844-v1+1_concur-cr.pdf","access_level":"open_access","creator":"system","file_size":335170,"content_type":"application/pdf"}]},{"scopus_import":"1","article_processing_charge":"No","has_accepted_license":"1","day":"31","page":"169 - 187","citation":{"ista":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of forwarding schemes in switched networks with probabilistic faults. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206, 169–187.","apa":"Avni, G., Goel, S., Henzinger, T. A., & Rodríguez Navas, G. (2017). Computing scores of forwarding schemes in switched networks with probabilistic faults (Vol. 10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54580-5_10","ieee":"G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores of forwarding schemes in switched networks with probabilistic faults,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.","ama":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:10.1007/978-3-662-54580-5_10","chicago":"Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas. “Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults,” 10206:169–87. Springer, 2017. https://doi.org/10.1007/978-3-662-54580-5_10.","mla":"Avni, Guy, et al. Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults. Vol. 10206, Springer, 2017, pp. 169–87, doi:10.1007/978-3-662-54580-5_10.","short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187."},"date_published":"2017-03-31T00:00:00Z","alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a "product-like" structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation. ","lang":"eng"}],"intvolume":" 10206","ddc":["000"],"title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","status":"public","_id":"1116","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa_version":"Submitted Version","file":[{"file_id":"4698","relation":"main_file","date_created":"2018-12-12T10:08:37Z","date_updated":"2018-12-12T10:08:37Z","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":321800}],"pubrep_id":"758","publication_identifier":{"issn":["03029743"]},"month":"03","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"quality_controlled":"1","isi":1,"oa":1,"external_id":{"isi":["000440733400010"]},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-54580-5_10","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"publist_id":"6246","file_date_updated":"2018-12-12T10:08:37Z","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","year":"2017","volume":10206,"date_created":"2018-12-11T11:50:14Z","date_updated":"2023-09-20T11:32:43Z","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy"},{"full_name":"Goel, Shubham","first_name":"Shubham","last_name":"Goel"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Rodríguez Navas","first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo"}]},{"abstract":[{"lang":"eng","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 overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology."}],"type":"conference","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","creator":"system","file_size":365172,"content_type":"application/pdf","file_id":"5249","relation":"main_file","date_updated":"2018-12-12T10:16:58Z","date_created":"2018-12-12T10:16:58Z"}],"pubrep_id":"818","status":"public","title":"An abstraction-refinement methodology for reasoning about network games","ddc":["004"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1003","day":"30","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","date_published":"2017-05-30T00:00:00Z","page":"70 - 76","citation":{"apa":"Avni, G., Guha, S., & Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press. https://doi.org/10.24963/ijcai.2017/11","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia, 2017, pp. 70–76.","ista":"Avni G, Guha S, Kupferman O. 2017. An abstraction-refinement methodology for reasoning about network games. IJCAI: International Joint Conference on Artificial Intelligence , 70–76.","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:10.24963/ijcai.2017/11","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games,” 70–76. AAAI Press, 2017. https://doi.org/10.24963/ijcai.2017/11.","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76.","mla":"Avni, Guy, et al. An Abstraction-Refinement Methodology for Reasoning about Network Games. AAAI Press, 2017, pp. 70–76, doi:10.24963/ijcai.2017/11."},"file_date_updated":"2018-12-12T10:16:58Z","publist_id":"6395","date_updated":"2023-09-22T09:49:00Z","date_created":"2018-12-11T11:49:38Z","author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"related_material":{"record":[{"id":"6006","status":"public","relation":"later_version"}]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"AAAI Press","year":"2017","month":"05","publication_identifier":{"issn":["10450823"]},"language":[{"iso":"eng"}],"conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence ","end_date":"2017-08-25","location":"Melbourne, Australia","start_date":"2017-08-19"},"doi":"10.24963/ijcai.2017/11","isi":1,"quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000764137500011"]},"oa":1},{"language":[{"iso":"eng"}],"conference":{"name":"EMSOFT: Embedded Software ","end_date":"2016-10-07","location":"Pittsburgh, PA, USA","start_date":"2016-10-01"},"doi":"10.1145/2968478.2968499","quality_controlled":"1","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"oa":1,"month":"10","date_created":"2018-12-11T11:50:20Z","date_updated":"2021-01-12T06:48:33Z","author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"first_name":"Guillermo","last_name":"Rodríguez Navas","full_name":"Rodríguez Navas, Guillermo"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"ACM","year":"2016","file_date_updated":"2018-12-12T10:09:31Z","ec_funded":1,"publist_id":"6223","article_number":"26","date_published":"2016-10-01T00:00:00Z","publication":"Proceedings of the 13th International Conference on Embedded Software ","citation":{"chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In Proceedings of the 13th International Conference on Embedded Software . ACM, 2016. https://doi.org/10.1145/2968478.2968499.","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” Proceedings of the 13th International Conference on Embedded Software , 26, ACM, 2016, doi:10.1145/2968478.2968499.","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in Proceedings of the 13th International Conference on Embedded Software , Pittsburgh, PA, USA, 2016.","apa":"Avni, G., Guha, S., & Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In Proceedings of the 13th International Conference on Embedded Software . Pittsburgh, PA, USA: ACM. https://doi.org/10.1145/2968478.2968499","ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: Proceedings of the 13th International Conference on Embedded Software . ACM; 2016. doi:10.1145/2968478.2968499"},"day":"01","has_accepted_license":"1","scopus_import":1,"file":[{"file_size":279240,"content_type":"application/pdf","creator":"system","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf","access_level":"open_access","date_created":"2018-12-12T10:09:31Z","date_updated":"2018-12-12T10:09:31Z","relation":"main_file","file_id":"4755"}],"oa_version":"Submitted Version","pubrep_id":"644","ddc":["000"],"status":"public","title":"Synthesizing time triggered schedules for switched networks with faulty links","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1135","abstract":[{"text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM.","lang":"eng"}],"type":"conference"},{"day":"01","has_accepted_license":"1","scopus_import":1,"date_published":"2016-09-01T00:00:00Z","page":"153 - 166","citation":{"ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 153–166.","apa":"Avni, G., Henzinger, T. A., & Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_13","ista":"Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:10.1007/978-3-662-53354-3_13","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games,” 9928:153–66. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_13.","short":"G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.","mla":"Avni, Guy, et al. Dynamic Resource Allocation Games. Vol. 9928, Springer, 2016, pp. 153–66, doi:10.1007/978-3-662-53354-3_13."},"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."}],"alternative_title":["LNCS"],"type":"conference","file":[{"file_name":"IST-2016-645-v1+1_sagt-cr.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":243458,"file_id":"5073","relation":"main_file","date_updated":"2020-07-14T12:44:45Z","date_created":"2018-12-12T10:14:22Z","checksum":"0825eefd4e22774f6f62cb7d7389b05a"}],"oa_version":"Preprint","pubrep_id":"645","ddc":["000"],"title":"Dynamic resource allocation games","status":"public","intvolume":" 9928","_id":"1341","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"09","language":[{"iso":"eng"}],"conference":{"end_date":"2016-09-21","location":"Liverpool, United Kingdom","start_date":"2016-09-19","name":"SAGT: Symposium on Algorithmic Game Theory"},"doi":"10.1007/978-3-662-53354-3_13","quality_controlled":"1","project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa":1,"file_date_updated":"2020-07-14T12:44:45Z","publist_id":"5926","ec_funded":1,"date_updated":"2023-08-17T13:52:49Z","date_created":"2018-12-11T11:51:28Z","volume":9928,"author":[{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"6761"}]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2016","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award)."}]