Strategy Synthesis for Zero-sum Neuro-symbolic Concurrent Stochastic Games (Extended Version)

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 probabilistic finite-state agents interacting in a shared continuous-state environment, observed through perception mechanisms implemented as neural networks. Since the environment state space is continuous, we focus on the class of NS-CSGs with Borel state spaces. We consider the problem of zero-sum discounted cumulative rewards and prove the existence of the value of NS-CSGs under Borel measurability and piecewise-constant restrictions on the components of the model. From an algorithmic perspective, existing methods to compute values and optimal strategies for CSGs focus on finite state spaces. We present, for the first time, implementable value iteration and policy iteration algorithms to solve a class of uncountable state space CSGs, namely NS-CSGs, and prove their convergence. Our approach works by exploiting the underlying game structures and then formulating piecewise linear or constant representations of the value functions and strategies of NS-CSGs. We illustrate our approach by applying a prototype implementation of value iteration to a dynamic vehicle parking case study.