Parameter synthesis techniques for continuous-time Markov chains have been described in [1,2] and implemented on top of the tool PRISM [3].

The goal of this thesis is to accelerate the current implementation [4] in order to make the parameter synthesis feasible for larger models. The student will first optimise the implementation using effective representation of the model based on sparse data structures. The main objective of the thesis is to design and implement a GPU acceleration of the parameter synthesis. The student is also required to provide a detailed experimental evaluation of the GPU implementation and compare it with the optimised sequential implementation on relevant models including biochemical models as well as models of computer and engineering systems.