  We present novel techniques for neuro-symbolic concurrent stochastic games, a
recently proposed modelling formalism to represent a set of probabilistic
agents operating in a continuous-space environment using a combination of
neural network based perception mechanisms and traditional symbolic methods. To
date, only zero-sum variants of the model were studied, which is too
restrictive when agents have distinct objectives. We formalise notions of
equilibria for these models and present algorithms to synthesise them. Focusing
on the finite-horizon setting, and (global) social welfare subgame-perfect
optimality, we consider two distinct types: Nash equilibria and correlated
equilibria. We first show that an exact solution based on backward induction
may yield arbitrarily bad equilibria. We then propose an approximation
algorithm called frozen subgame improvement, which proceeds through iterative
solution of nonlinear programs. We develop a prototype implementation and
demonstrate the benefits of our approach on two case studies: an automated
car-parking system and an aircraft collision avoidance system.
