×

An abstraction-refinement methodology for reasoning about network games. (English) Zbl 1418.91097

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

MSC:

91A43 Games involving graphs
05C57 Games on graphs (graph-theoretic aspects)
68Q45 Formal languages and automata

Software:

NetworkX; GameShrink
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Fabrikant, A.; Luthra, A.; Maneva, E.; Papadimitriou, C.; Shenker, S.; On a Network Creation Game; Proceedings of the ACM Symposium on Principles of Distributed Computing: ; . · Zbl 1322.91013
[2] Albers, S.; Elits, S.; Even-Dar, E.; Mansour, Y.; Roditty, L.; On Nash Equilibria for a Network Creation Game; Proceedings of the 7th ACM-SIAM Symposium on Discrete Algorithms: ; . · Zbl 1192.91036
[3] Anshelevich, E.; Dasgupta, A.; Kleinberg, J.; Tardos, E.; Wexler, T.; Roughgarden, T.; The Price of Stability for Network Design with Fair Cost Allocation; SIAM J. Comput.: 2008; Volume 38 ,1602-1623. · Zbl 1173.91321
[4] Rosenthal, R.W.; A class of games possessing pure-strategy Nash equilibria; Int. J. Game Theory: 1973; Volume 2 ,65-67. · Zbl 0259.90059
[5] Roughgarden, T.; Tardos, E.; How bad is selfish routing?; J. ACM: 2002; Volume 49 ,236-259. · Zbl 1323.90011
[6] Nash, J.; Equilibrium points in n-person games; Proc. Natl. Acad. Sci. USA: 1950; Volume 36 ,48-49. · Zbl 0036.01104
[7] Tardos, E.; Wexler, T.; Network Formation Games and the Potential Function Method; Algorithmic Game Theory: Cambridge, UK 2007; . · Zbl 1152.91315
[8] Meyers, C.A.; Network Flow Problems and Congestion Games: Complexity and Approximation Results; Ph.D. Thesis: Cambridge, MA, USA 2006; .
[9] Fabrikant, A.; Papadimitriou, C.; Talwar, K.; The complexity of pure Nash equilibria; Proceedings of the 36th ACM Symp. on Theory of Computing: ; ,604-612. · Zbl 1192.91042
[10] Syrgkanis, V.; The Complexity of Equilibria in Cost Sharing Games; Lecture Notes in Computer Science, Proceedings of the International Workshop on Internet and Network Economics, Stanford, CA, USA, 13-17 December 2010: Berlin, Germany 2010; Volume Volume 6484 ,366-377.
[11] Johnson, D.S.; Papadimtriou, C.H.; Yannakakis, M.; How Easy is Local Search?; J. Comput. Syst. Sci.: 1988; Volume 37 ,79-100. · Zbl 0655.68074
[12] Babichenko, Y.; Query Complexity of Approximate Nash Equilibria; J. ACM: 2016; Volume 63 ,36. · Zbl 1407.91016
[13] Rubinstein, A.; Settling the Complexity of Computing Approximate Two-Player Nash Equilibria; Proceedings of the 57th IEEE Symposium on Foundations of Computer Science: ; ,258-265.
[14] Zhang, J.; Pourazarm, S.; Cassandras, C.G.; Paschalidis, I.C.; The Price of Anarchy in Transportation Networks: Data-Driven Evaluation and Reduction Strategies; Proc. IEEE: 2018; Volume 106 ,538-553.
[15] Koutsoupias, E.; Papadimitriou, C.; Worst-case equilibria; Comput. Sci. Rev.: 2009; Volume 3 ,65-69. · Zbl 1303.91012
[16] Newman, M.; The Structure and Function of Complex Networks; SIAM Rev.: 2003; Volume 45 ,167-256. · Zbl 1029.68010
[17] Barabási, A.L.; ; Linked-How Everything Is Connected to Everything Else and What It Means for Business, Science, and Everyday Life: New York, NY, USA 2003; .
[18] Paluch, R.; Lu, X.; Suchecki, K.; Szymański, B.K.; Holyst, J.A.; Fast and accurate detection of spread source in large complex networks; Sci. Rep.: 2018; Volume 8 ,1-10.
[19] Clarke, E.; Grumberg, O.; Peled, D.; ; Model Checking: Cambridge, MA, USA 1999; . · Zbl 0847.68063
[20] Cousot, P.; Cousot, R.; Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints; Proceedings of the 4th ACM Symposium on Principles of Programming Languages: ; ,238-252.
[21] Larsen, K.; Modal Specifications; Lecture Notes in Computer Science, Proceedings of the International Conference on Computer Aided Verification, Grenoble, France, 12-14 June 1989: Berlin, Germany 1989; Volume Volume 407 ,232-246.
[22] Dams, D.; Gerth, R.; Grumberg, O.; Abstract interpretation of reactive systems; ACM Trans. Programm. Lang. Syst.: 1997; Volume 19 ,253-291.
[23] Bruns, G.; Godefroid, P.; Model Checking Partial State Spaces with 3-Valued Temporal Logics; Proceedings of the International Conference on Computer Aided Verification: ; ,274-287. · Zbl 1046.68583
[24] Shoham, S.; Grumberg, O.; Monotonic Abstraction-Refinement for CTL; Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems: ; Volume Volume 2988 ,546-560. · Zbl 1126.68487
[25] Clarke, E.M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H.; Counterexample-guided abstraction refinement for symbolic model checking; J. ACM: 2003; Volume 50 ,752-794. · Zbl 1325.68145
[26] Gilpin, A.; Sandholm, T.; Lossless Abstraction of Imperfect Information Games; J. ACM: 2007; Volume 54 ,25. · Zbl 1314.91025
[27] Brown, N.; Sandholm, T.; Simultaneous Abstraction and Equilibrium Finding in Games; Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence: ; ,489-496.
[28] Gilpin, A.; Sandholm, T.; Sørensen, T.B.; A Heads-up No-limit Texas Hold’Em Poker Player: Discretized Betting Models and Automatically Generated Equilibrium-finding Programs; Proceedings of the 7th International Joint Conference on Autonomous Agents and Multiagent Systems: ; ,911-918.
[29] Alur, R.; Henzinger, T.; Kupferman, O.; Vardi, M.; Alternating refinement relations; Proceedings of the International Conference on Concurrency Theory: ; Volume Volume 1466 ,163-178. · Zbl 1070.68524
[30] Henzinger, T.; Majumdar, R.; Mang, F.; Raskin, J.F.; Abstract Interpretation of Game Properties; Proceedings of the International Static Analysis Symposium: ; Volume Volume 1824 ,245-252. · Zbl 0966.68150
[31] De Alfaro, L.; Godefroid, P.; Jagadeesan, R.; Three-Valued Abstractions of Games: Uncertainty, but with Precision; Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science: ; ,170-179.
[32] Ball, T.; Kupferman, O.; An Abstraction-Refinement Framework for Multi-Agent Systems; Proceedings of the 21st IEEE Symposium on Logic in Computer Science: ; .
[33] Gutierrez, J.; Harrenstein, P.; Perelli, G.; Wooldridge, M.; Nash Equilibrium and Bisimulation Invariance; Proceedings of the 28th International Conference on Concurrency Theory: ; Volume Volume 85 ,1-16.
[34] Gutierrez, J.; Harrenstein, P.; Wooldridge, M.; Iterated Boolean games; Inf. Comput.: 2015; Volume 242 ,53-79. · Zbl 1318.91012
[35] Avni, G.; Kupferman, O.; Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction; Proceedings of the 23rd International Conference on Concurrency Theory: ; Volume Volume 7454 ,84-99. · Zbl 1364.68242
[36] Daniele, N.; Guinchiglia, F.; Vardi, M.; Improved automata generation for linear temporal logic; Proceedings of the 11th International Conference on Computer Aided Verification: ; Volume Volume 1633 ,249-260. · Zbl 1046.68588
[37] Avni, G.; Kupferman, O.; Tamir, T.; Network-formation games with regular objectives; Inf. Comput.: 2016; Volume 251 ,165-178. · Zbl 1353.91012
[38] Vissicchio, S.; Vanbever, L.; Bonaventure, O.; Opportunities and research challenges of hybrid software defined networks; Comput. Commun. Rev.: 2014; Volume 44 ,70-75.
[39] Conitzer, V.; Sandholm, T.; New complexity results about Nash equilibria; Games Econ. Behav.: 2008; Volume 63 ,621-641. · Zbl 1142.91365
[40] Hagberg, A.A.; Schult, D.A.; Swart, P.; Exploring network structure, dynamics, and function using NetworkX; Proceedings of the 7th Python in Science Conference (SciPy2008): ; ,11-15.
[41] Godefroid, P.; Huth, M.; Jagadeesan, R.; Abstraction-based Model Checking using Modal Transition Systems; Proceedings of the 12th International Conference on Concurrency Theory: ; Volume Volume 2154 ,426-440. · Zbl 1006.68077
[42] Avni, G.; Kupferman, O.; Tamir, T.; Congestion and Cost-Sharing Games with Multisets of Resources; Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science: ; . · Zbl 1369.91007
[43] Alur, R.; Henzinger, T.; Kupferman, O.; Alternating-time temporal logic; J. ACM: 2002; Volume 49 ,672-713. · Zbl 1326.68181
[44] Chatterjee, K.; Henzinger, T.A.; Piterman, N.; Strategy logic; Inf. Comput.: 2010; Volume 208 ,677-693. · Zbl 1205.68197
[45] Mogavero, F.; Murano, A.; Perelli, G.; Vardi, M.Y.; Reasoning About Strategies: On the Model-Checking Problem; ACM Trans. Comput. Log.: 2014; Volume 15 ,34. · Zbl 1354.68178
[46] Chatterjee, K.; Henzinger, T.A.; Jurdzinski, M.; Games with secure equilibria; Theor. Comput. Sci.: 2006; Volume 365 ,67-82. · Zbl 1108.91007
[47] Chatterjee, K.; Nash Equilibrium for Upward-Closed Objectives; Proceedings of the 15th Annual Conference on the European Association for Computer Science Logic: ; Volume Volume 4207 ,271-286. · Zbl 1225.91009
[48] Fisman, D.; Kupferman, O.; Lustig, Y.; Rational Synthesis; Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: ; Volume Volume 6015 ,190-204. · Zbl 1284.68396
[49] Almagor, S.; Avni, G.; Kupferman, O.; Repairing Multi-Player Games; Proceedings of the 26th International 26th Conference on Concurrency: ; Volume Volume 42 ,325-339. · Zbl 1374.68317
[50] Chatterjee, K.; Majumdar, R.; Jurdzinski, M.; On Nash Equilibria in Stochastic Games; Proceedings of the 13th Annual Conference on the European Association for Computer Science Logic: ; Volume Volume 3210 ,26-40. · Zbl 1095.91001
[51] Brihaye, T.; Bruyère, V.; De Pril, J.; Gimbert, H.; On Subgame Perfection in Quantitative Reachability Games; arXiv: 2012; . · Zbl 1352.68146
[52] Avni, G.; Henzinger, T.; Kupferman, O.; Dynamic Resource Allocation Games; Proceedings of the International Symposium on Algorithmic Game Theory: ; Volume Volume 9928 ,153-166. · Zbl 1403.91059
[53] Avni, G.; Guha, S.; Kupferman, O.; Timed Network Games; Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science: ; Volume Volume 83 ,1-16.
[54] Avni, G.; Guha, S.; Kupferman, O.; Timed Network Games with Clocks; Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science: ; Volume Volume 117 .
[55] Kupferman, O.; Tamir, T.; Hierarchical Network Formation Games; Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems: ; Volume Volume 10205 ,229-246.
[56] Glusman, M.; Kamhi, G.; Mador-Haim, S.; Fraer, R.; Vardi, M.; Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation; Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: ; Volume Volume 2619 ,176-191. · Zbl 1031.68549
[57] Pistore, M.; Traverso, P.; Planning as Model Checking for Extended Goals in Non-deterministic Domains; Proceedings of the 17th International Joint Conference on Artificial Intelligence: ; .
[58] Filar, J.; Vrieze, K.; ; Competitive Markov Decision Processes: Berlin, Germany 1996; . · Zbl 0934.91002
[59] Sutton, R.S.; Barto, A.G.; Reinforcement learning—An introduction; Adaptive Computation and Machine Learning: Cambridge, MA, USA 1998; .
[60] Michalak, T.; Rahwan, T.; Wooldridge, M.; Strategic Social Network Analysis; Proceedings of the 31st Conference on Artificial Intelligence: ; ,4841-4845.
[61] Sandholm, T.; Algorithm for optimal winner determination in combinatorial auctions; Artif. Intell.: 2002; Volume 135 ,1-54. · Zbl 0984.68039
[62] Fatima, S.; Kraus, S.; Wooldridge, M.; ; Principles of Automated Negotiation: Cambridge, UK 2014; .
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.