Seminars

Sodium-Potassium Exchange Pump Model and Analysis with Probabilistic Model Checking PDF files
Sérgio Campos - Universidade Federal de Minas Gersia, Brazil

07/11/2011, 10am, GHC-8102

Abstract

Recently there has been a growing interest in the application of Probabilistic Model Checking (PMC) for the formal specification of biological systems. PMC is able to exhaustively explore all states of a stochastic model and can provide valuable insight into its behavior which are more difficult to see using only traditional methods for system analysis such as deterministic and stochastic simulation. In this work we propose a stochastic modeling for the description and analysis of sodium-potassium exchange pump.  The sodium-potassium pump is a membrane transport system presents in all animal cell and capable of moving sodium and potassium ions against their concentration gradient.

We present a quantitative formal specification of the pump mechanism in the PRISM language, taking into consideration a discrete chemistry approach and the Law of Mass Action aspects. We also present an analysis of the system using quantitative properties in order to verify the pump reversibility and understand the pump behavior using trend labels for the transition rates of the pump reactions.

Probabilistic model checking can be used along with other well established approaches such as simulation and differential equations to better understand pump behavior.  Using PMC we can determine if specific events happen such as "the potassium outside the cell ends in all model traces". We can also have a more detailed perspective on its behavior such as determining its reversibility and why its normal operation becomes slow over time. This knowledge can be used to direct experimental research and make it more efficient, leading to faster and more accurate scientific discoveries.

Biography

Sérgio V. Campos has received the bachelors degree in computer science from Universidade Federal de Minas Gerais (Belo Horizonte - Brasil) in 1986, the masters degree in computer science from the same university in 1990 and the Ph.D. degree in Computer Science from Carnegie Mellon University in 1996 on the topic of formal verification of real-time systems. Sérgio is currently an associate professor at the Computer Science Department of Universidade Federal de Minas Gerais. While at UFMG Sérgio has worked on various topics such as formal verification of hardware and software, the design and implementation of multimedia systems, scheduling problems and telecommunication network management.

His interests include design, analysis and verification of real-time systems, hardware and software in general. More recently Sérgio has worked on Bioinformatics and Systems Biology, implementing biological data management systems and verifying biological systems behavior.