IEEE/ACM Trans Comput Biol Bioinform. 2021 Nov-Dec;18(6):2816-2822. doi: 10.1109/TCBB.2020.3028776. Epub 2021 Dec 8.
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.
研究生物系统是一项困难但重要的任务。传统的方法包括实验室实验和计算机模拟。然而，研究人员通常需要探索重要但潜在罕见的事件，这些事件不容易观察或模拟。我们使用 UPPAAL-SMC，这是一种形式验证工具，支持一种方法，使我们能够对生物系统进行建模，指定我们想要分析的事件和条件，并使用受控模拟来探索系统执行情况。我们还描述了一种在计算机上重现实验室实验的有效方法。与传统模拟不同，我们能够通过将这些条件表示为时间逻辑公式来指导实验探索特殊事件和条件。我们已经将这种方法应用于创建比以前更详细的 Palytoxin 诱导的 Na /K 泵通道模型。此外，我们已经重现了实验方案及其相关的电生理记录，这在以前的工作中没有做到。因此，我们能够提出 PTX 泵复合物的新二聚体模型并研究其行为。我们方法的使用使我们能够减少执行这项研究的工作和时间。它可以用于对其他复杂的生物系统进行建模和分析，从而提高此类研究的效率。
