  Probabilistic model checking for stochastic games enables formal verification
of systems that comprise competing or collaborating entities operating in a
stochastic environment. Despite good progress in the area, existing approaches
focus on zero-sum goals and cannot reason about scenarios where entities are
endowed with different objectives. In this paper, we propose probabilistic
model checking techniques for concurrent stochastic games based on Nash
equilibria. We extend the temporal logic rPATL (probabilistic alternating-time
temporal logic with rewards) to allow reasoning about players with distinct
quantitative goals, which capture either the probability of an event occurring
or a reward measure. We present algorithms to synthesise strategies that are
subgame perfect social welfare optimal Nash equilibria, i.e., where there is no
incentive for any players to unilaterally change their strategy in any state of
the game, whilst the combined probabilities or rewards are maximised. We
implement our techniques in the PRISM-games tool and apply them to several case
studies, including network protocols and robot navigation, showing the benefits
compared to existing approaches.
