Concurrent Reachability Games
=============================
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 $ e > 0$ a randomized strategy to reach the target with
probability greater than $1 - e$.
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.