Concurrent reachability games |
| |
Authors: | Luca de Alfaro Thomas A Henzinger Orna Kupferman |
| |
Affiliation: | 1. Department of Computer Engineering, University of California, Santa Cruz, USA;2. Computer and Communication Sciences, EPFL, Lausanne, Switzerland;3. School of Computer Science and Engineering, Hebrew University, Jerusalem, Israel |
| |
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: | Games Reachability Stochastic games Concurrent games |
本文献已被 ScienceDirect 等数据库收录! |
|