Abstraction-based Synthesis of Stochastic Hybrid Systems

In this work, we develop a framework for formally constructing finite abstractions, also known as finite Markov decision processes (MDPs), for continuous-space stochastic hybrid systems. These complex systems encompass both continuous dynamics, described by stochastic differential equations involving Brownian motions and Poisson processes, as well as instantaneous jumps governed by stochastic difference equations with additive noise components. Our approach is grounded in the concept of stochastic simulation functions, enabling us to employ finite MDPs as suitable substitutes for original hybrid systems in the controller design process. Our construction methodology offers an augmented framework capable of characterizing stochastic hybrid systems with both continuous evolutions and instantaneous jumps. This unified framework ensures that state trajectories of augmented systems exactly match those of original hybrid systems. Subsequently, we outline a systematic procedure for constructing finite MDPs from the general class of nonlinear stochastic hybrid systems exhibiting an incremental input-to-state stability property. Additionally, we focus on a linear class of stochastic hybrid systems and propose a construction scheme based on the satisfaction of certain matrix inequalities. We validate the efficacy of our proposed approaches through a case study.