Concurrent reachability games Journal Article

Author(s): de Alfaro, Luca; Henzinger, Thomas A; Kupferman, Orna
Article Title: Concurrent reachability games
Abstract: We consider concurrent two-player games with reachability objectives. In such games, at each round, player 1 and player 2 independently and simultaneously choose moves, and the two choices determine the next state of the game. The objective of player 1 is to reach a set of target states; the objective of player 2 is to prevent this. These are zero-sum games, and the reachability objective is one of the most basic objectives: determining the set of states from which player 1 can win the game is a fundamental problem in control theory and system verification. There are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε>0 a randomized strategy to reach the target with probability greater than 1−ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies.
Keywords: stochastic games; games; reachability; concurrent games
Journal Title: Theoretical Computer Science
Volume: 386
Issue 3
ISSN: 0304-3975
Publisher: Elsevier  
Date Published: 2007-11-01
Start Page: 188
End Page: 217
DOI: 10.1016/j.tcs.2007.07.008
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work