Modelagem e análise de sistemas de transporte de íons em membranas celulares usando verificação de modelos

Abstract

Recently there has been a growing interest in the application of Probabilistic Model Checking (PMC) for the formal specification and analysis 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 the use of PMC for the modeling and analysis of cell membrane systems that are capable of moving ions across cell membranes and are crucial for the living cells. We present a quantitative formal specification of sodium-potassium exchange pump (Na,K-ATPase), which is an important transport system present in all animal cells and responsible for keeping the potassium and sodium concentrations inside the cell, respectively, high and low. We describe how the pump mechanism can be modeled using PMC, taking into consideration different modeling methodologies in order to deal with the state space explosion problem, inherent in model checking, regardless of context. Furthermore, we present some important properties about the pump reversibility that can be addressed directly with model checking, whereas with other traditional approaches they cannot be easily covered. Aditionally, we reason about the pump behavior in terms of trend labels for the pump reactions that compute if there is a greater probability that the system takes specific transitions. These trends allow us to identify the bottlenecks that are responsible for the slow operation of the Na,K-ATPase or even for its interruption over time. The work also introduces an approach to detect noisy periodic behavior in stochastic systems using a statistical probabilistic model checking. The proposed approach is applied to the intracellular calcium oscillations, which is membrane system commonly observed in a large number of cell types in response to stimulation by an extracellular agonist. Finally a modeling methodology to deal with the coexistences of species with huge differences in their concentrations is also introduced. Although the results are still preliminary, they indicate gains in scalability of memory resources using the proposed methodology.