## Concurrent Reachability Games

*Luca de Alfaro,
Thomas A. Henzinger,
and Orna Kupferman*

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.

*Theoretical Computer Science* 386:188-217, 2007.
A preliminary version appeared in the
*Proceedings of the
39th Annual Symposium on Foundations of Computer Science*
(FOCS), IEEE Computer Society Press, 1998, pp. 564-575.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1997 IEEE,
2007 Springer.