In Silico Laboratory Experiments Using Statistical Model Checking: A New Model of the Palytoxin-Induced Pump Channel as Case Study.

Studying biological systems is a difficult but important task. Traditional methods include laboratory experimentation and computer simulations. However, often researchers need to explore important but potentially rare events that are not easily observed or simulated. We use UPPAAL-SMC, a formal verification tool to support a methodology that allows us to model biological systems, specify events and conditions that we want to analyze, and to explore system executions using controlled simulations. We also describe an efficient way to reproduce laboratory experiments in silico. Unlike traditional simulations, we are able to guide the experiment to explore special events and conditions by expressing these conditions in temporal logic formulas. We have applied this methodology to create a more detailed model of Palytoxin-induced Na +/K + pump channels than was previously possible. Moreover, we have reproduced experimental protocols and their associated electrophysiological recordings, which has not been done in previous works. As a consequence, we have been able to propose a new diprotomeric model for the PTX-pump complex and study its behaviour. The use of our methodology has enabled us to reduce the effort and time to perform this research. It can be used to model and analyze other complex biological systems, potentially increasing the productivity of such studies.

Hypothesized diprotomeric enzyme complex supported by stochastic modelling of palytoxin-induced Na/K pump channels.

The sodium-potassium pump (Na+/K+ pump) is crucial for cell physiology. Despite great advances in the understanding of this ionic pumping system, its mechanism is not completely understood. We propose the use of a statistical model checker to investigate palytoxin (PTX)-induced Na+/K+ pump channels. We modelled a system of reactions representing transitions between the conformational substates of the channel with parameters, concentrations of the substates and reaction rates extracted from simulations reported in the literature, based on electrophysiological recordings in a whole-cell configuration. The model was implemented using the UPPAAL-SMC platform. Comparing simulations and probabilistic queries from stochastic system semantics with experimental data, it was possible to propose additional reactions to reproduce the single-channel dynamic. The probabilistic analyses and simulations suggest that the PTX-induced Na+/K+ pump channel functions as a diprotomeric complex in which protein-protein interactions increase the affinity of the Na+/K+ pump for PTX.