  We study turn-based stochastic zero-sum games with lexicographic preferences
over reachability and safety objectives. Stochastic games are standard models
in control, verification, and synthesis of stochastic reactive systems that
exhibit both randomness as well as angelic and demonic non-determinism.
Lexicographic order allows to consider multiple objectives with a strict
preference order over the satisfaction of the objectives. To the best of our
knowledge, stochastic games with lexicographic objectives have not been studied
before. We establish determinacy of such games and present strategy and
computational complexity results. For strategy complexity, we show that
lexicographically optimal strategies exist that are deterministic and memory is
only required to remember the already satisfied and violated objectives. For a
constant number of objectives, we show that the relevant decision problem is in
NP $\cap$ coNP, matching the current known bound for single objectives; and in
general the decision problem is PSPACE-hard and can be solved in NEXPTIME
$\cap$ coNEXPTIME. We present an algorithm that computes the lexicographically
optimal strategies via a reduction to computation of optimal strategies in a
sequence of single-objectives games. We have implemented our algorithm and
report experimental results on various case studies.
