The complexity of solving reachability games using value and strategy iteration

Concurrent reachability games is a class of games heavily studied by the computer science community, in particular by the formal methods community. Two standard algorithms for approximately solving two-player zero-sum concurrent reachability games are value iteration and strategy iteration. A rigorous complexity analysis of these algorithms has been an open problem until now. We prove a lower bound of 2m(N) on the worst case number of iterations needed for both of these algorithms to provide non-trivial approximations to the value of a game with N non-terminal positions and m actions for each player in each position. In particular, both algorithms have at least doubly-exponential complexity. Also, even when the game given as input has only one non-terminal position, we prove an exponential lower bound on their time complexities. The instances establishing the lower bound may be regarded as natural rather than pathological and our proofs of the lower bounds proceed by arguing about the...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Kristoffer Arnsfelt Hansen, Rasmus Ibsen-Jensen, Peter Bro Miltersen
• Keywords: Algorithms, Concurrent Reachability Games, CORR 2010, Education, Lower Bound