Jan 24, 2012: Dragan Bosnacki: Efficient Probabilistic Model Checking on GPUs & Some Applications of Probabilistic Model Checking to Biological Systems

January 24, 2012Efficient Probabilistic Model Checking on GPUs & Some Applications of Probabilistic Model Checking to Biological Systems
Room: Zi 5126Dragan Bosnacki
12:30-13:30

In the first part of my talk I will present efficient parallel algorithms for probabilistic model checking on general purpose graphic processing units (GPGPUs). The crucial idea is to improve the numerical parts of the traditional sequential algorithms. In particular, we capitalize on the fact that in most of them operations like matrix–vector multiplication and solving systems of linear equations are the main complexity bottlenecks. Since linear algebraic operations can be implemented very efficiently on GPGPUs, the new parallel algorithms show considerable runtime improvements compared to their counterparts on standard architectures. We implemented our parallel algorithms on top of the probabilistic model checker PRISM. The prototype implementation was evaluated on several case studies in which we observed significant speedups over the standard CPU implementation of the tool.

Probabilistic model checking can be used very effectively to model biological systems. In many such cases model checking can replace successfully stochastic simulations. The second part of the talk will be about a stochastic model of the translation of mRNA into proteins, which is one of the basic processes in the cell. With this model one can analyze the errors that occur in the synthesized proteins as well as the translation times that are needed to translate specific mRNAs. Besides their fundamental importance, this kind of models have potential applications in the development of antibiotics and for an industrial scale biosynthesis of proteins. I will also argue that the presented model is a representative of an interesting class of biological problems that can be tackled by probabilistic model checking.