...
首页> 外文期刊>BMC Genomics >Modeling and analysis of cell membrane systems with probabilistic model checking
【24h】

Modeling and analysis of cell membrane systems with probabilistic model checking

机译:利用概率模型检查对细胞膜系统进行建模和分析

获取原文
           

摘要

BackgroundRecently 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.ResultsWe 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.ConclusionsProbabilistic 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.
机译:背景技术近来,对于概率模型检查(PMC)在生物学系统的正式规范中的应用越来越引起人们的兴趣。 PMC能够穷举探索随机模型的所有状态,并且可以提供对它的行为的宝贵见解,而仅使用传统方法进行系统分析(例如确定性和随机模拟)就很难发现它的行为。在这项工作中,我们提出了一种用于描述和分析钠钾交换泵的随机模型。钠钾泵是存在于所有动物细胞中的膜运输系统,能够使钠和钾离子逆着其浓度梯度移动。结果我们考虑了离散化学方法,提出了PRISM语言中泵机制的定量形式规格以及《群众行动法》方面。我们还使用定量属性对系统进行了分析,以验证泵的可逆性并使用趋势标签来了解泵反应的转换率,从而了解泵的行为。结论概率模型检查可以与其他完善的方法(例如模拟)一起使用和微分方程,以更好地了解泵的性能。使用PMC,我们可以确定是否发生特定事件,例如所有模型迹线中细胞外部的钾末端。我们还可以对它的行为有更详细的了解,例如确定它的可逆性以及为什么它的正常运行会随着时间而变慢。这些知识可用于指导实验研究并使其更有效,从而导致更快,更准确的科学发现。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号