Symbolic control of stochastic switched systems via finite abstractions

Abstract

Stochastic switched systems are a class of continuous-time dynamical models with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. As such, they represent a subclass of general stochastic hybrid systems. While the literature has witnessed recent progress in the dynamical analysis and controller synthesis for the stability of stochastic switched systems, more complex and challenging objectives related to the verification of and the synthesis for logic specifications (properties expressed as formulas in linear temporal logic or as automata on infinite strings) have not been formally investigated as of yet. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, a finite symbolic model that is approximately bisimilar to a stochastic switched system is constructed under some dynamical stability assumptions on the concrete model. This allows to formally synthesize controllers (switching signals) over the finite symbolic model that are valid for the concrete system, by means of mature techniques in the literature. © 2013 Springer-Verlag.