A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria

Pedro A. Góngora; David A. Rosenblueth

International Journal of Applied Mathematics and Computer Science (2015)

  • Volume: 25, Issue: 3, page 577-596
  • ISSN: 1641-876X

Abstract

top
Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman-Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.

How to cite

top

Pedro A. Góngora, and David A. Rosenblueth. "A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria." International Journal of Applied Mathematics and Computer Science 25.3 (2015): 577-596. <http://eudml.org/doc/271794>.

@article{PedroA2015,
abstract = {Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman-Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.},
author = {Pedro A. Góngora, David A. Rosenblueth},
journal = {International Journal of Applied Mathematics and Computer Science},
keywords = {shortest path; Bellman-Ford; Nash equilibrium; BDD; model checking; binary decision diagram (BDD)},
language = {eng},
number = {3},
pages = {577-596},
title = {A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria},
url = {http://eudml.org/doc/271794},
volume = {25},
year = {2015},
}

TY - JOUR
AU - Pedro A. Góngora
AU - David A. Rosenblueth
TI - A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
JO - International Journal of Applied Mathematics and Computer Science
PY - 2015
VL - 25
IS - 3
SP - 577
EP - 596
AB - Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman-Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.
LA - eng
KW - shortest path; Bellman-Ford; Nash equilibrium; BDD; model checking; binary decision diagram (BDD)
UR - http://eudml.org/doc/271794
ER -

References

top
  1. Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A. and Somenzi, F. (1997). Algebraic decision diagrams and their applications, Formal Methods in System Design 10(2-3): 171-206. 
  2. Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking, MIT Press, New York, NY. Zbl1179.68076
  3. Berghammer, R. and Bolus, S. (2012). On the use of binary decision diagrams for solving problems on simple games, European Journal of Operational Research 222(3): 529-541. Zbl1253.91014
  4. Bolus, S. (2011). Power indices of simple games and vector-weighted majority games by means of binary decision diagrams, European Journal of Operational Research 210(2): 258-272. Zbl1210.91012
  5. Bonanno, G. (2001). Branching time, perfect information games, and backward induction, Games and Economic Behavior 36(1): 57-73. Zbl0987.91006
  6. Bryant, R.E. (1986). Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers 35(8): 677-691. Zbl0593.94022
  7. Burch, J., Clarke, E., McMillan, K., Dill, D. and Hwang, L. (1992). Symbolic model checking: 1020 states and beyond, Information and Computation 98(2): 142-170. Zbl0753.68066
  8. Clarke, E. and Emerson, E. (1982). Design and synthesis of synchronization skeletons using branching time temporal logic, in D. Kozen (Ed.), Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131, Springer, Berlin/Heidelberg, pp. 52-71. Zbl0546.68014
  9. Clarke, E.M., Emerson, E.A. and Sistla, A.P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8(2): 244-263. Zbl0591.68027
  10. Clarke, E.M., Grumberg, O. and Peled, D.A. (1999). Model Checking, MIT Press, London. 
  11. Clarke, E., McMillan, K., Zhao, X., Fujita, M. and Yang, J. (1993). Spectral transforms for large Boolean functions with applications to technology mapping, 30th Conference on Design Automation, Dallas, TX, USA, pp. 54-60. 
  12. Cormen, T.H., Leiserson, C.E., Rivest, R.L. and Stein, C. (2009). Introduction to Algorithms, 3rd Edn., MIT Press, Cambridge, MA. Zbl1187.68679
  13. Dasgupta, P., Chakrabarti, P.P., Deka, J.K. and Sankaranarayanan, S. (2001). Min-max computation tree logic, Artificial Intelligence 127(1): 137-162. Zbl0976.68104
  14. Dsouza, A. and Bloom, B. (1995). Generating BDD models for process algebra terms, Proceedings of the 7th International Conference on Computer Aided Verification, Liège, Belgium, pp. 16-30. 
  15. Enders, R., Filkorn, T. and Taubner, D. (1992). Generating BDDs for symbolic model checking in CCS, Proceedings of the 3rd International Workshop on Computer Aided Verification, CAV'91, London, UK, pp. 203-213. Zbl0778.68063
  16. Fujita, M., McGeer, P.C. and Yang, J.C.-Y. (1997). Multi-terminal binary decision diagrams: An efficient data structure for matrix representation, Formal Methods in System Design 10(2-3): 149-169. 
  17. Garroppo, R.G., Giordano, S. and Tavanti, L. (2010). A survey on multi-constrained optimal path computation: Exact and approximate algorithms, Computer Networks 54(17): 3081-3107. Zbl1210.68138
  18. Harrenstein, P., van der Hoek, W., Meyer, J.-J.C. and Witteveen, C. (2003). A modal characterization of Nash equilibrium, Fundamenta Informaticae 57(2-4): 281-321. Zbl1041.03016
  19. Hermanns, H., Meyer-Kayser, J. and Siegle, M. (1999). Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains, in B. Plateau, W.J. Stewart and M. Silva (Eds.), 3rd International Workshop on the Numerical Solution of Markov Chains, Zaragoza, Spain, Prensas Universitarias de Zaragoza, Zaragoza, pp. 188-207. 
  20. Kelley, Jr, J.E. and Walker, M.R. (1959). Critical-path planning and scheduling, Eastern Joint IRE-AIEE-ACM Computer Conference, Boston, MA, USA, pp. 160-173. 
  21. Lozovanu, D. and Pickl, S. (2009). Optimization and Multiobjective Control of Time-Discrete Systems, Springer, Berlin/Heidelberg. Zbl1166.93001
  22. McKelvey, R.D. and McLennan, A. (1996). Computation of equilibria in finite games, in H.M. Amman, D.A. Kendrick and J. Rust (Eds.), Handbook of Computational Economics, Vol. 1, Elsevier, North Holland, Chapter 2, pp. 87-142. Zbl1126.91304
  23. McKelvey, R.D., McLennan, A.M. and Turocy, T.L. (2014). Gambit: Software tools for game theory, version 13.1.2, http://www.gambit-project.org. 
  24. Meinel, C. and Theobald, T. (1998). Algorithms and Data Structures in VSLI Design: OBDD-Foundations and Applications, Springer-Verlag, Berlin. Zbl0899.68040
  25. MSDN (2013). Memory limits for windows releases, Microsoft Developer Network, http://msdn.microsoft.com/en-us/library/windows/desktop/aa366778(v=vs.85).aspx. 
  26. Osborne, M.J. and Rubinstein, A. (1994). A Course in Game Theory, The MIT Press, Cambridge, MA. Zbl1194.91003
  27. Raimondi, F. and Lomuscio, A. (2007). Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Journal of Applied Logic 5(2): 235-251. Zbl1122.68076
  28. Russell, S. and Norvig, P. (2003). Artificial Intelligence. A Modern Approach, Prentince Hall, Englewood Cliffs, NJ. Zbl0835.68093
  29. Sawitzki, D. (2004). Experimental studies of symbolic shortest-path algorithms, in C.C. Ribeiro and S.L. Martins (Eds.), Experimental and Efficient Algorithms, Lecture Notes in Computer Science, Vol. 3059, Springer, Berlin/Heidelberg, pp. 482-497. 
  30. Tarapata, Z. (2007). Selected multicriteria shortest path problems: An analysis of complexity, models and adaptation of standard algorithms, International Journal of Applied Mathematics and Computer Science 17(2): 269-287, DOI: 10.2478/v10006-007-0023-2. Zbl1120.93051

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.