conference paper published yes Luca De Alfaro author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Orna Kupferman author FOCS: Foundations of Computer Science An open system can be modeled as a two-player game between the system and its environment. At each round of the game, player 1 (the system) and player 2 (the environment) independently and simultaneously choose moves, and the two choices determine the next state of the game. Properties of open systems can be modeled as objectives of these two-player games. For the basic objective of reachability-can player 1 force the game to a given set of target states?-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 ε&gt;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. Finally, we apply our results by introducing a temporal logic in which all three kinds of winning conditions can be specified, and which can be model checked in polynomial time. This logic, called Randomized ATL, is suitable for reasoning about randomized behavior in open (two-agent) as well as multi-agent systems IEEE1998Palo Alto, CA, United States of America eng 081869172710.1109/SFCS.1998.743507 564 - 575 yes De Alfaro, L., Henzinger, T. A., &#38; Kupferman, O. (1998). Concurrent reachability games. In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i> (pp. 564–575). Palo Alto, CA, United States of America: IEEE. <a href="https://doi.org/10.1109/SFCS.1998.743507  ">https://doi.org/10.1109/SFCS.1998.743507  </a> De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability Games.” In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, 564–75. IEEE, 1998. <a href="https://doi.org/10.1109/SFCS.1998.743507  ">https://doi.org/10.1109/SFCS.1998.743507  </a>. De Alfaro, Luca, et al. “Concurrent Reachability Games.” <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, IEEE, 1998, pp. 564–75, doi:<a href="https://doi.org/10.1109/SFCS.1998.743507  ">10.1109/SFCS.1998.743507  </a>. L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability games,” in <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, Palo Alto, CA, United States of America, 1998, pp. 564–575. De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. In: <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>. IEEE; 1998:564-575. doi:<a href="https://doi.org/10.1109/SFCS.1998.743507  ">10.1109/SFCS.1998.743507  </a> L. De Alfaro, T.A. Henzinger, O. Kupferman, in:, Proceedings 39th Annual Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–575. De Alfaro L, Henzinger TA, Kupferman O. 1998. Concurrent reachability games. Proceedings 39th Annual Symposium on Foundations of Computer Science. FOCS: Foundations of Computer Science, 564–575. 46392018-12-11T12:09:53Z2022-08-22T14:09:02Z