  Rational verification is the problem of determining which temporal logic
properties will hold in a multi-agent system, under the assumption that agents
in the system act rationally, by choosing strategies that collectively form a
game-theoretic equilibrium. Previous work in this area has largely focussed on
deterministic systems. In this paper, we develop the theory and algorithms for
rational verification in probabilistic systems. We focus on concurrent
stochastic games (CSGs), which can be used to model uncertainty and randomness
in complex multi-agent environments. We study the rational verification problem
for both non-cooperative games and cooperative games in the qualitative
probabilistic setting. In the former case, we consider LTL properties satisfied
by the Nash equilibria of the game and in the latter case LTL properties
satisfied by the core. In both cases, we show that the problem is
2EXPTIME-complete, thus not harder than the much simpler verification problem
of model checking LTL properties of systems modelled as Markov decision
processes (MDPs).
