Departamento de Ciencias de la Computación, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México México D.F., México.
Front Plant Sci. 2012 Jul 20;3:155. doi: 10.3389/fpls.2012.00155. eCollection 2012.
Model checking is a well-established technique for automatically verifying complex systems. Recently, model checkers have appeared in computer tools for the analysis of biochemical (and gene regulatory) networks. We survey several such tools to assess the potential of model checking in computational biology. Next, our overview focuses on direct applications of existing model checkers, as well as on algorithms for biochemical network analysis influenced by model checking, such as those using binary decision diagrams (BDDs) or Boolean-satisfiability solvers. We conclude with advantages and drawbacks of model checking for the analysis of biochemical networks.
模型检查是一种用于自动验证复杂系统的成熟技术。最近，模型检查器出现在用于分析生化（和基因调控）网络的计算机工具中。我们调查了几个这样的工具，以评估模型检查在计算生物学中的潜力。接下来，我们的概述重点关注现有模型检查器的直接应用，以及受模型检查影响的生化网络分析算法，例如使用二进制决策图（BDD）或布尔可满足性求解器的算法。最后，我们总结了模型检查用于分析生化网络的优缺点。
