  Neuro-symbolic approaches to artificial intelligence, which combine neural
networks with classical symbolic techniques, are growing in prominence,
necessitating formal approaches to reason about their correctness. We propose a
novel modelling formalism called neuro-symbolic concurrent stochastic games
(NS-CSGs), which comprise two probabilistic finite-state agents interacting in
a shared continuous-state environment. Each agent observes the environment
using a neural perception mechanism, which converts inputs such as images into
symbolic percepts, and makes decisions symbolically. We focus on the class of
NS-CSGs with Borel state spaces and prove the existence and measurability of
the value function for zero-sum discounted cumulative rewards under
piecewise-constant restrictions on the components of this class of models. To
compute values and synthesise strategies, we present, for the first time,
practical value iteration (VI) and policy iteration (PI) algorithms to solve
this new subclass of continuous-state CSGs. These require a finite
decomposition of the environment induced by the neural perception mechanisms of
the agents and rely on finite abstract representations of value functions and
strategies closed under VI or PI. First, we introduce a Borel measurable
piecewise-constant (B-PWC) representation of value functions, extend minimax
backups to this representation and propose a value iteration algorithm called
B-PWC VI. Second, we introduce two novel representations for the value
functions and strategies, constant-piecewise-linear (CON-PWL) and
constant-piecewise-constant (CON-PWC) respectively, and propose
Minimax-action-free PI by extending a recent PI method based on alternating
player choices for finite state spaces to Borel state spaces, which does not
require normal-form games to be solved.
