---
_id: '4639'
abstract:
- lang: eng
  text: '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 ε>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'
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: 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.
  ista: '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.'
  mla: 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>.
  short: L. De Alfaro, T.A. Henzinger, O. Kupferman, in:,  Proceedings 39th Annual
    Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–575.
conference:
  end_date: 1998-11-11
  location: Palo Alto, CA, United States of America
  name: 'FOCS: Foundations of Computer Science'
  start_date: 1998-11-08
date_created: 2018-12-11T12:09:53Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-22T14:09:02Z
day: '01'
doi: '10.1109/SFCS.1998.743507  '
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 564 - 575
publication: ' Proceedings 39th Annual Symposium on Foundations of Computer Science'
publication_identifier:
  isbn:
  - '0818691727'
publication_status: published
publisher: IEEE
publist_id: '68'
quality_controlled: '1'
status: public
title: Concurrent reachability games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1998'
...