Bisimilar Symbolic Models for Stochastic Switched Systems: A Discretization-Free Approach

In the past few years several techniques have been developed to construct symbolic models of continuous-time stochastic (hybrid) systems. The constructed symbolic models can be used to compute hybrid controllers enforcing rich human-readable specifications on the original concrete systems. Unfortunately, most of the existing techniques suffer severely from the curse of dimensionality because of the continuous space discretization: the sizes of the symbolic models grow exponentially with the dimension of the continuous space. In this paper, we provide a novel technique to construct symbolic models for a class of stochastic hybrid systems, namely, stochastic switched systems, without any continuous space discretization. We show that for any incrementally stable stochastic switched system and any given precision epsilon, one can construct an epsilon-approximate bisimilar symbolic model of the original system without any continuous space discretization. Therefore, the proposed technique is potentially more efficient than the existing ones when dealing with higher dimensional stochastic switched systems. The effectiveness of the proposed results is illustrated by synthesizing a controller regulating temperatures of a six-room building by employing its symbolic model which is not tractable using existing approaches based on the continuous space discretization.