×

Determinacy in discrete-bidding infinite-duration games. (English) Zbl 1509.91007

Summary: 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.

MSC:

91A43 Games involving graphs
68Q45 Formal languages and automata
91A50 Discrete-time games

References:

[1] S. Almagor, G. Avni, and O. Kupferman. Repairing multi-player games. InProc. 26th CONCUR, pages 325-339, 2015. · Zbl 1374.68317
[2] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic.J. ACM, 49(5):672-713, 2002. · Zbl 1326.68181
[3] B. Aminof and S. Rubin. First-cycle games.Inf. Comput., 254:195-216, 2017. · Zbl 1371.91019
[4] K.R. Apt and E. Gr¨adel.Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. · Zbl 1214.91003
[5] N. Atzei, M. Bartoletti, and T. Cimoli. A survey of attacks on ethereum smart contracts.IACR Cryptology ePrint Archive, 2016:1007, 2016.
[6] G. Avni, S. Guha, and O. Kupferman. An abstraction-refinement methodology for reasoning about network games. InProc. 26th IJCAI, pages 70-76, 2017. · Zbl 1418.91097
[7] G. Avni, T. A. Henzinger, and V. Chonev. Infinite-duration bidding games.J. ACM, 66(4):31:1-31:29, 2019. · Zbl 1448.91060
[8] G. Avni, T. A. Henzinger, and R. Ibsen-Jensen. Infinite-duration poorman-bidding games. InProc. 14th WINE, volume 11316 ofLNCS, pages 21-36. Springer, 2018. · Zbl 1443.91070
[9] G. Avni, T. A. Henzinger, and O. Kupferman. Dynamic resource allocation games. InProc. 9th SAGT, pages 153-166, 2016. · Zbl 1403.91059
[10] G. Avni, T. A. Henzinger, and ¯D. ˇZikeli´c. Bidding mechanisms in graph games. InIn Proc. 44th MFCS, volume 138 ofLIPIcs, pages 11:1-11:13, 2019. · Zbl 1539.91027
[11] G. Avni, R. Ibsen-Jensen, and J. Tkadlec. All-pay bidding games on graphs.Proc. 34th AAAI, 2020.
[12] G. Avni, O. Kupferman, and T. Tamir. Network-formation games with regular objectives.Inf. Comput., 251:165-178, 2016. · Zbl 1353.91012
[13] J. Bhatt and S. Payne. Bidding chess.Math. Intelligencer, 31:37-39, 2009. · Zbl 1328.00021
[14] T. Brihaye, V. Bruy‘ere, J. De Pril, and H. Gimbert. On subgame perfection in quantitative reachability games.Logical Methods in Computer Science, 9(1), 2012. · Zbl 1352.68146
[15] K. Chatterjee. Nash equilibrium for upward-closed objectives. InProc. 15th CSL, volume 4207 ofLecture Notes in Computer Science, pages 271-286. Springer, 2006. · Zbl 1225.91009
[16] K. Chatterjee, A. K. Goharshady, and Y. Velner. Quantitative analysis of smart contracts. InProc. 27th ESOP, pages 739-767, 2018. · Zbl 1418.68024
[17] K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Games with secure equilibria.Theor. Comput. Sci., 365(1-2):67-82, 2006. · Zbl 1108.91007
[18] K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic.Inf. Comput., 208(6):677-693, 2010. · Zbl 1205.68197
[19] K. Chatterjee, R. Majumdar, and M. Jurdzinski. On nash equilibria in stochastic games. InProc. 13th CSL, pages 26-40, 2004. · Zbl 1095.91001
[20] A. Condon. On algorithms for simple stochastic games. InProc. DIMACS, pages 51-72, 1990. · Zbl 0808.90141
[21] M. Develin and S. Payne. Discrete bidding games.The Electronic Journal of Combinatorics, 17(1):R85, 2010. · Zbl 1188.91048
[22] E.A. Emerson and C. Jutla. Tree automata,µ-calculus and determinacy. InProc. 32nd IEEE Symp. on Foundations of Computer Science, pages 368-377, 1991.
[23] H. Everett. Recursive games.Annals of Mathematics Studies, 3(39):47-78, 1955. · Zbl 0078.32802
[24] D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. InProc. 16th TACAS, pages 190-204, 2010. · Zbl 1284.68396
[25] E. Gr¨adel, W. Thomas, and T. Wilke.Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 ofLecture Notes in Computer Science. Springer, 2002.
[26] O. Kupferman and T. Tamir. Hierarchical network formation games. InProc. 23rd TACAS, pages 229-246, 2017. · Zbl 1457.91106
[27] A. J. Lazarus, D. E. Loeb, J. G. Propp, W. R. Stromquist, and D. H. Ullman. Combinatorial games under auction play.Games and Economic Behavior, 27(2):229-264, 1999. · Zbl 0949.91001
[28] A. J. Lazarus, D. E. Loeb, J. G. Propp, and D. Ullman. Richman games.Games of No Chance, 29:439-449, 1996.
[29] D. A. Martin. The determinacy of blackwell games.J. Symb. Log., 63(4):1565-1581, 1998. · Zbl 0926.03071
[30] D.A. Martin. Borel determinacy.Annals of Mathematics, 65:363-371, 1975. · Zbl 0336.02049
[31] R. Meir, G. Kalai, and M. Tennenholtz. Bidding games and efficient allocations.Games and Economic Behavior, 2018. · Zbl 1419.91072
[32] M. Menz, J. Wang, and J. Xie. Discrete all-pay bidding games.CoRR, abs/1504.02799, 2015.
[33] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem.ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. · Zbl 1354.68178
[34] S. Muthukrishnan. Ad exchanges: Research issues. InProc. 5th WINE, pages 1-12, 2009.
[35] N. Nisan, T. Roughgarden, E. Tardos, and V. Vazirani.Algorithmic Game Theory. Cambridge University Press, 2007. · Zbl 1130.91005
[36] Y. Peres, O. Schramm, S. Sheffield, and D. B. Wilson. Tug-of-war and the infinity laplacian.J. Amer. Math. Soc., 22:167-210, 2009. · Zbl 1206.91002
[37] A. Pnueli and R. Rosner. On the synthesis of a reactive module. InProc. 16th POPL, pages 179-190, 1989. · Zbl 0686.68015
[38] M.O. Rabin. Decidability of second order theories and automata on infinite trees.Transaction of the AMS, 141:1-35, 1969. · Zbl 0221.02031
[39] S. Le Roux. Concurrent games and semi-random determinacy. InProc. 43rd MFCS, pages 40:1-40:15, 2018. · Zbl 1512.91023
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.