Approximately bisimilar symbolic models for randomly switched stochastic systems

In the past few years there has been a growing interest in the use of symbolic models for control systems. The main reason is the possibility to leverage algorithmic techniques over symbolic models to synthesize controllers that are valid for the concrete control systems. Such controllers can enforce complex logical specifications that are otherwise hard (if not impossible) to establish on the concrete models with classical control techniques. Examples of such specifications include those expressible via linear temporal logic or as automata on infinite strings. A relevant goal in this research line is in the identification of classes of systems that admit symbolic models: in particular, continuous-time systems with stochastic or hybrid dynamics have been only recently considered, due to their rather general and complex dynamics. In this work we make progress in this direction by enlarging the class of stochastic hybrid systems admitting finite, symbolic models: specifically, we show that randomly switched stochastic systems, satisfying some incremental stability assumption, admit such models.