--- _id: '4544' abstract: - lang: eng text: We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. We present in this paper a strategy improvement algorithm for computing the value of a concurrent safety game, that is, the maximal probability with which player 1 can enforce the safety objective. The algorithm yields a sequence of player-1 strategies which ensure probabilities of winning that converge monotonically to the value of the safety game. Our result is significant because the strategy improvement algorithm provides, for the first time, a way to approximate the value of a concurrent safety game from below. Since a value iteration algorithm, or a strategy improvement algorithm for reachability games, can be used to approximate the same value from above, the combination of both algorithms yields a method for computing a converging sequence of upper and lower bounds for the values of concurrent reachability and safety games. Previous methods could approximate the values of these games only from one direction, and as no rates of convergence are known, they did not provide a practical way to solve these games. author: - first_name: Krishnendu full_name: Krishnendu Chatterjee id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: de Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Termination criteria for solving concurrent safety and reachability games. In: SIAM; 2009:197-206. doi:10.1137/1.9781611973068.23' apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2009). Termination criteria for solving concurrent safety and reachability games (pp. 197–206). Presented at the SODA: Symposium on Discrete Algorithms, SIAM. https://doi.org/10.1137/1.9781611973068.23' chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Termination Criteria for Solving Concurrent Safety and Reachability Games,” 197–206. SIAM, 2009. https://doi.org/10.1137/1.9781611973068.23. ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Termination criteria for solving concurrent safety and reachability games,” presented at the SODA: Symposium on Discrete Algorithms, 2009, pp. 197–206.' ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2009. Termination criteria for solving concurrent safety and reachability games. SODA: Symposium on Discrete Algorithms, 197–206.' mla: Chatterjee, Krishnendu, et al. Termination Criteria for Solving Concurrent Safety and Reachability Games. SIAM, 2009, pp. 197–206, doi:10.1137/1.9781611973068.23. short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, SIAM, 2009, pp. 197–206. conference: name: 'SODA: Symposium on Discrete Algorithms' date_created: 2018-12-11T12:09:24Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:59:35Z day: '01' doi: 10.1137/1.9781611973068.23 extern: 1 file: - access_level: open_access checksum: ce7dc1667502e26b23c07a767ac41ae6 content_type: application/pdf creator: system date_created: 2018-12-12T10:08:03Z date_updated: 2020-07-14T12:46:31Z file_id: '4662' file_name: IST-2012-37-v1+1_Termination_criteria_for_solving_concurrent_safety_and_reachability_games.pdf file_size: 212369 relation: main_file file_date_updated: 2020-07-14T12:46:31Z main_file_link: - open_access: '1' url: https://repository.ist.ac.at/id/eprint/37 month: '01' oa: 1 page: 197 - 206 publication_status: published publisher: SIAM publist_id: '176' pubrep_id: '37' quality_controlled: 0 status: public title: Termination criteria for solving concurrent safety and reachability games type: conference year: '2009' ...