Stochastic Hybrid Systems provide a powerful modelling framework and allow to tackle applications in such areas as engineering, systems biology, finance etc. Such models can be analyzed against complex specifications such as “What is the maximal probability that the blackout never happens in the power network and what is the action sequence maximizing such probability”. Specifications like that can be written using modal logics like LTL, which provides both the handy way to express properties of interest, and the way to reduce their analysis to several basic problems.

Since the specifications as above are quantitative (involve the probability of an event or an expected value of some random variable), their computation may be unfeasible over the original model. Due to this reason, we exploit notions of approximate abstractions to estimate the quantities of interest with a guaranteed precision. In particular, we use formula-free abstractions for the finite-horizon properties, and formula-guided one for the infinite-horizon ones. One of the message to be conveyed within this talk is that working with stochastic systems requires solid knowledge of probabilistic methods: this does not only lead to results of greater abstract generality, but also to the results which are more computationally efficient. The talk is concluded with a brief computational example from the insurance.