  Concurrent stochastic games (CSGs) are an ideal formalism for modelling
probabilistic systems that feature multiple players or components with distinct
objectives making concurrent, rational decisions. Examples include
communication or security protocols and multi-robot navigation. Verification
methods for CSGs exist but are limited to scenarios where agents or players are
grouped into two coalitions, with those in the same coalition sharing an
identical objective. In this paper, we propose multi-coalitional verification
techniques for CSGs. We use subgame-perfect social welfare (or social cost)
optimal Nash equilibria, which are strategies where there is no incentive for
any coalition to unilaterally change its strategy in any game state, and where
the total combined objectives are maximised (or minimised). We present an
extension of the temporal logic rPATL (probabilistic alternating-time temporal
logic with rewards) to specify equilibria-based properties for any number of
distinct coalitions, and a corresponding model checking algorithm for a variant
of stopping games. We implement our techniques in the PRISM-games tool and
apply them to several case studies, including a secret sharing protocol and a
public good game.
