online read us now
Paper details
Number 3 - September 2015
Volume 25 - 2015
A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
Pedro A. Góngora, David A. Rosenblueth
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.
Keywords
shortest path, Bellman–Ford, Nash equilibrium, BDD, model checking