Topological superposition of abstractions of stochastic processes

In this paper, we present a sound integration mechanism for Markov processes that are abstractions of stochastic hybrid systems (SHS). In a previous work, we have defined a very general model of SHS and we proved that the realization of an SHS is a Markov process. Moreover, we have developed a verification strategy for the reachability analysis problem. We develop further this line of research by making verification modularly. To achieve this, the state space is decomposed into regions that might share a common border. An abstraction can be constructed on each region and the abstraction method can vary from one region to another. We show how these abstractions can be integrated to provide an abstraction for the entire system. We illustrate this technique for the reachability analysis problem.