  Game-theoretic concepts have been extensively studied in economics to provide
insight into competitive behaviour and strategic decision making. As computing
systems increasingly involve concurrently acting autonomous agents,
game-theoretic approaches are becoming widespread in computer science as a
faithful modelling abstraction. These techniques can be used to reason about
the competitive or collaborative behaviour of multiple rational agents with
distinct goals or objectives. This paper provides an overview of recent
advances in developing a modelling, verification and strategy synthesis
framework for concurrent stochastic games implemented in the probabilistic
model checker PRISM-games. This is based on a temporal logic that supports
finite- and infinite-horizon temporal properties in both a zero-sum and
nonzero-sum setting, the latter using Nash and correlated equilibria with
respect to two optimality criteria, social welfare and social fairness. We
summarise the key concepts, logics and algorithms and the currently available
tool support. Future challenges and recent progress in adapting the framework
and algorithmic solutions to continuous environments and neural networks are
also outlined.
