---
res:
bibo_abstract:
- '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@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Luca
foaf_name: de Alfaro, Luca
foaf_surname: De Alfaro
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Orna
foaf_name: Kupferman, Orna
foaf_surname: Kupferman
bibo_doi: '10.1109/SFCS.1998.743507 '
dct_date: 1998^xs_gYear
dct_publisher: IEEE@
dct_title: Concurrent reachability games@
...