Using chemical organization theory for model checking

被引:18
|
作者
Kaleta, Christoph [1 ,2 ,3 ]
Richter, Stephan [1 ,2 ]
Dittrich, Peter [1 ,2 ]
机构
[1] Univ Jena, JCB, Bio Syst Anal Grp, D-07743 Jena, Germany
[2] Univ Jena, Dept Math & Comp Sci, D-07743 Jena, Germany
[3] Univ Jena, Dept Bioinformat, D-07743 Jena, Germany
关键词
SIGNAL-TRANSDUCTION; NETWORKS; SYSTEMS; PATHWAY; MECHANISMS;
D O I
10.1093/bioinformatics/btp332
中图分类号
Q5 [生物化学];
学科分类号
071010 ; 081704 ;
摘要
Motivation: The increasing number and complexity of biomodels makes automatic procedures for checking the models' properties and quality necessary. Approaches like elementary mode analysis, flux balance analysis, deficiency analysis and chemical organization theory (OT) require only the stoichiometric structure of the reaction network for derivation of valuable information. In formalisms like Systems Biology Markup Language (SBML), however, information about the stoichiometric coefficients required for an analysis of chemical organizations can be hidden in kinetic laws. Results: First, we introduce an algorithm that uncovers stoichiometric information that might be hidden in the kinetic laws of a reaction network. This allows us to apply OT to SBML models using modifiers. Second, using the new algorithm, we performed a large-scale analysis of the 185 models contained in the manually curated BioModels Database. We found that for 41 models (22%) the set of organizations changes when modifiers are considered correctly. We discuss one of these models in detail (BIOMD149, a combined model of the ERK- and Wnt-signaling pathways), whose set of organizations drastically changes when modifiers are considered. Third, we found inconsistencies in 5 models (3%) and identified their characteristics. Compared with flux-based methods, OT is able to identify those species and reactions more accurately [in 26 cases (14%)] that can be present in a long-term simulation of the model. We conclude that our approach is a valuable tool that helps to improve the consistency of biomodels and their repositories.
引用
收藏
页码:1915 / 1922
页数:8
相关论文
共 50 条
  • [1] Model checking using automata theory
    Peled, D
    [J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 55 - 79
  • [2] Model Checking Using SMT and Theory of Lists
    Milicevic, Aleksandar
    Kugler, Hillel
    [J]. NASA FORMAL METHODS, 2011, 6617 : 282 - +
  • [3] A Proof Theory for Model Checking
    Quentin Heath
    Dale Miller
    [J]. Journal of Automated Reasoning, 2019, 63 : 857 - 885
  • [4] A theory of hints in model checking
    Kaltenbach, M
    Misra, J
    [J]. FORMAL METHODS AT THE CROSSROADS: FROM PANACEA TO FOUNDATIONAL SUPPORT, 2003, 2757 : 423 - 438
  • [5] Distributed CTL model checking using MapReduce: theory and practice
    Camilli, Carlo Bellettini Matteo
    Capra, Lorenzo
    Monga, Mattia
    [J]. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2016, 28 (11): : 3025 - 3041
  • [6] A Proof Theory for Model Checking
    Heath, Quentin
    Miller, Dale
    [J]. JOURNAL OF AUTOMATED REASONING, 2019, 63 (04) : 857 - 885
  • [7] Model checking: Theory into practice
    Emerson, EA
    [J]. FST TCS 2000: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2000, 1974 : 1 - 10
  • [8] Automatic symmetry detection for model checking using computational group theory
    Donaldson, AF
    Miller, A
    [J]. FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 481 - 496
  • [9] Model checking: From tools to theory
    Alur, Rajeev
    [J]. 25 YEARS OF MODEL CHECKING: HISTORY, ACHIEVEMENTS, PERSPECTIVES, 2008, 5000 : 89 - 106
  • [10] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    [J]. MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221