de Alfaro, Luca ; Henzinger, Thomas AIST Austria ; Kupferman, Orna
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.
Theoretical Computer Science
188 - 217
De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. Theoretical Computer Science. 2007;386(3):188-217. doi:10.1016/j.tcs.2007.07.008
De Alfaro, L., Henzinger, T. A., & Kupferman, O. (2007). Concurrent reachability games. Theoretical Computer Science, 386(3), 188–217. https://doi.org/10.1016/j.tcs.2007.07.008
De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability Games.” Theoretical Computer Science 386, no. 3 (2007): 188–217. https://doi.org/10.1016/j.tcs.2007.07.008.
L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability games,” Theoretical Computer Science, vol. 386, no. 3, pp. 188–217, 2007.
De Alfaro L, Henzinger TA, Kupferman O. 2007. Concurrent reachability games. Theoretical Computer Science. 386(3), 188–217.
De Alfaro, Luca, et al. “Concurrent Reachability Games.” Theoretical Computer Science, vol. 386, no. 3, Elsevier, 2007, pp. 188–217, doi:10.1016/j.tcs.2007.07.008.