Model Checking Stochastic Hybrid Systems

Title: Model Checking Stochastic Hybrid Systems

Speaker: E. Moritz Hahn (Inst. of Software, CAS)

Time: 14:00, Thursday, 6 June, 2013

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

 The interplay of random phenomena with discrete-continuous dynamics deserves increased attention in many systems of growing importance.

Their verification needs to consider both stochastic behaviour and hybrid dynamics. In the verification of classical hybrid systems, one is often interested in deciding whether unsafe system states can be reached. In the stochastic setting, we ask instead whether the probability of reaching particular states is bound by a given threshold. In this talk, we consider stochastic hybrid systems and develop a general abstraction framework for deciding such problems. This gives rise to the first mechanisable technique that can, in practice, formally verify safety properties of systems which feature all the relevant aspects of nondeterminism, general continuous-time dynamics, and probabilistic behaviour. Being based tools for classical hybrid systems, future improvements in the effectivity of such tools directly carry over to improvements in the effectivity of our technique.

We extend the method in several directions: First, we discuss how we can handle continuous probability distributions. We then consider systems which we are in partial control of. Next, we consider systems in which probabilities are parametric, to analyse entire system families at once. Afterwards, we consider systems equipped with rewards, modelling costs or bonuses. Finally, we consider all orthogonal combinations of the extensions to the core model.

Ernst Moritz Hahn received his B.Sc. degree from Carl von Ossietzky University Oldenburg in 2005, M.Sc degree from Saarland University in

2008 and Ph.D. also from Saarland University in 2013. He wrote his doctoral thesis at the chair of Dependable Systems and Software, advised

by Holger Hermanns. After his dissertation, he became research assistant at the group of automated verification at the University of Oxford in the VERIWARE project lead by Marta Kwiatkowska. Ernst Moritz Hahn is currently associate professor in the Institute of

Software Chinese Academy of Sciences. His research area is in probabilistic verification, in particular of stochastic hybrid systems.

He is also interested in the verification of very large Markov chains and parametric Markov models. In these areas, he was also involved in

the development of several software tools. His research has been sponsored by grants from the German Research Foundation, the European

Research Council, and the Argentine Ministerio de Ciencia, Tecnologia e Innovacion Productiva.