Approximate abstractions of discrete-time controlled stochastic hybrid systems

This work presents a procedure to construct a finite abstraction of a controlled discrete-time stochastic hybrid system. The state space and the control space of the original system are partitioned by finite lattices, according to some refinement parameters. The errors introduced by the abstraction procedure can be explicitly computed, over time, given some continuity assumptions on the original model. We show that the errors can be arbitrarily tuned by selecting the partition accuracy. The obtained abstraction can be interpreted as a controlled Markov set-Chain, and can be used both for verification and control design purposes. We test the proposed technique to analyze a model from systems biology.