### From State Key Laboratory of Computer Science

Professional Title: | Associate Research Professor |

Research Fields: | Probabilistic Model Checking |

Tel: | 010-62661604 |

E-Mail: | moritz(at)ios.ac.cn |

Abstractions of Stochastic Hybrid Systems. Stochastic hybrid systems not only involve both continuous time and a continuous state space, but also stochastic behaviors. Here, we focus on adding probabilities to the discrete jumps a hybrid system can perform. This way we have a nondeterministic choice of distributions over successor states. Initially, we have focused on distributions with finite support. We described a method to use existing tools for non-probabilistic hybrid systems for reachability analyses to compute safe bounds for the unbounded reachability probability in a stochastic hybrid system.

In a parametric Markov chain, certain aspects of a system are given as parameters instead of concrete numbers. Analyses then result in formulae over these parameters instead of single values. In addition to the basic model of discrete-time Markov chains, one can consider parametric Markov decision processes, which combine underspecified probabilities with nondeterministic choices, so that their analysis is more involved than the one of the basic model.

Process Calculi for Stochastic Hybrid Systems. In a recent paper, we extended the modelling language Modest to include hybrid aspects. Modest is a very expressive modelling language based on process calculi, which already covers timed and probabilistic aspects, including continuous distributions. Our extension mainly consists of including ordinary differential equations. This required severe extensions of both syntax and semantics of the Modest language. Doing so, we can harvest our previous results in the area of stochastic hybrid systems.

Variable Probabilistic Abstraction Refinement. Predicate abstraction has proven powerful in the analysis of very large probabilistic systems, but has thus far been limited to the analysis of systems with a fixed number of distinct transition probabilities. This excludes a large variety of potential analysis cases, ranging from sensor networks to biochemical systems, in which transition probabilities are given as a function of state variables. We extended existing abstraction techniques to handle such variable probabilities by using an extension of constraint or interval Markov chains.

Analysis of Markov chains. In a parametric Markov chain, certain aspects of a system are given as parameters instead of concrete numbers. Analyses then result in formulae over these parameters instead of single values. A further part of my work involves truncation-based analysis of very large Markov chains. Here, an infinite model is explored only to the extent needed to decide a given property. This method is very promising in various contexts. I am also involved in works about probabilistic predicate abstraction and related methods.

For the model classes described above, I developed analysis methods along with corresponding model checking tools.