Description

Parametric Markov chains occur quite naturally in various applications. In a recent paper (https://arxiv.org/abs/1805.05672), we have discussed how we can speed up the analysis of such models. The idea is to represent measures such as reachability probabilities, expected rewards, etc. as algebraic circuits, that is, as DAG-like structures. Once one has such an algebraic circuit, one can efficiently obtain the concrete value for a given instantiation of the parameter values. Using interval arithmetic, it is also possible to obtain lower and upper bounds for such values for regions of parameters. This can thus be used to decide for which parameter regions the value is guaranteed to be above or below a given threshold. Using GPGPU-based frameworks such as CUDA or OpenCL, the evaluation of parameter regions could be parallelised efficiently. Doing so, one can thus efficiently divide the parameter space into regions for which a given safety or performance measure is guaranteed to be above or below a given threshold.
Other details: A student wanting to do this project should be able to understand the cited paper, at least the basic ideas. Good programming skills are required. They should also know either CUDA or OpenCL, or at least be willing to learn the concepts of one of these frameworks very quickly. They should also either know or be willing to learn about interval arithmetic. The difficulty of this project is probably high. It will however probably lead to a (at least) workshop publication once finished.