Scalable Synthesis of Finite MDPs for Large-Scale Stochastic Switching Systems

This work is concerned with a scalable approach for constructing finite Markov decision processes (MDPs) as finite abstractions of large-scale discrete-time stochastic systems with Markovian switching signals. Our proposed framework deals with two different sources of adversary inputs: (i) bounded disturbances as the effects of other subsystems, and (ii) Markovian switching signals which are randomly changing in a finite set of modes. We leverage the notion of stochastic simulation functions (SSF) to quantify the probabilistic distance between original interconnected switching systems and their finite abstractions while providing guaranteed error bounds. We then utilize small-gain compositionality conditions to construct SSF between interconnected systems based on stochastic pseudo-simulation functions (SPSF), established between individual subsystems. For a particular class of nonlinear stochastic switching systems with incremental quadratic constraints on nonlinearity, we propose matrix-inequality conditions required for the construction of their SPSF. We verify our results over a nonlinear network of 100 subsystems (totally 200 dimensions) with Markovian switching signals by compositionally constructing a finite MDP for the network.