@article{4626,
  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.},
  author       = {de Alfaro, Luca and Thomas Henzinger and Kupferman, Orna},
  journal      = {Theoretical Computer Science},
  number       = {3},
  pages        = {188 -- 217},
  publisher    = {Elsevier},
  title        = {{Concurrent reachability games}},
  doi          = {10.1016/j.tcs.2007.07.008},
  volume       = {386},
  year         = {2007},
}