This Article 
 Bibliographic References 
 Add to: 
On Parameter Synthesis by Parallel Model Checking
May-June 2012 (vol. 9 no. 3)
pp. 693-705
A. Streck, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
A. Krejci, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
L. Brim, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
J. Barnat, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
D. Safranek, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
M. Vejnar, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
T. Vejpustek, Fac. of Inf., Masaryk Univ., Brno, Czech Republic
An important problem in current computational systems biology is to analyze models of biological systems dynamics under parameter uncertainty. This paper presents a novel algorithm for parameter synthesis based on parallel model checking. The algorithm is conceptually universal with respect to the modeling approach employed. We introduce the algorithm, show its scalability, and examine its applicability on several biological models.

[1] H. Kitano, "Systems Biology: A Brief Overview," Science, vol. 295, no. 5560, pp. 1662-1664, 2002.
[2] F. Horn and R. Jackson, "General Mass Action Kinetics," Archive for Rational Mechanics and Analysis, vol. 47, pp. 81-116, 1972.
[3] D. Thieffry and R. Thomas, "Dynamical Behavior of Biological Regulatory Networks," Bull. of Math. Biology, vol. 57, no. 2, pp. 277-297, 1995.
[4] H. de Jong et al., "Genetic Network Analyzer: Qualitative Simulation of Genetic Regulatory Networks," Bioinformatics, vol. 19, no. 3, pp. 336-344, 2003.
[5] Y. Kaznessis, "Models for Synthetic Biology," BMC Systems Biology, vol. 1, no. 47, 2007.
[6] S. Kay, Fundamentals of Statistical Signal Processing: Estimation Theory (volume 1), Prentice Hall, 1993.
[7] M. Rodriguez-Fernandez et al., "A Hybrid Approach for Efficient and Robust Parameter Estimation in Biochemical Pathways," Biosystems, vol. 83, nos. 2/3, pp. 248-265, 2006.
[8] P. Lindner and B. Hitzmann, "Experimental Design for Optimal Parameter Estimation of an Enzyme Kinetic Process Based on the Analysis of the Fisher Information Matrix," J. Theoretical Biology, vol. 238, no. 1, pp. 111-123, 2006.
[9] D. Battogtokh et al., "Bifurcation Analysis of a Model of the Budding Yeast Cell Cycle," Chaos, vol. 14, no. 3, pp. 653-661, 2004.
[10] D. Angeli et al., "Detection of Multistability, Bifurcations, and Hysteresis in a Large Class of Biological Positive-Feedback Systems," Proc. Nat'l Academy of Sciences USA, vol. 101, no. 7, pp. 1822-1827, 2004.
[11] J. Lu, H.W. Engl, R. Machné, and P. Schuster, "Inverse Bifurcation Analysis of a Model for the Mammalian g1/s Regulatory Module," Proc. Int'l Conf. Bioinformatics Research and Development (BIRD '07), pp. 168-184, 2007.
[12] T.A. Henzinger and H. Wong-Toi, "Using Hytech to Synthesize Control Parameters for a Steam Boiler," Proc. Formal Methods for Industrial Applications, pp. 265-282, 1995.
[13] G. Frehse et al., "A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata," Proc. Int'l Workshop Hybrid Systems: Computation and Control (HSCC), pp. 187-200, 2008.
[14] G. Batt et al., "Robustness Analysis and Tuning of Synthetic Gene Networks," Bioinformatics, vol. 23, no. 18, pp. 2415-2422, 2007.
[15] B. Yordanov and C. Belta, "Parameter Synthesis for Piecewise Affine Systems from Temporal Logic Specifications," Proc. Int'l Workshop Hybrid Systems: Computation and Control, vol. 4981, pp. 542-555, 2008.
[16] A. Donzé, B. Krogh, and A. Rajhans, "Parameter Synthesis for Hybrid Systems with an Application to Simulink Models," Proc. Int'l Conf. Hybrid Systems: Computation and Control (HSCC), pp. 165-179, 2009.
[17] E.M. Clarke et al., Model Checking. MIT Press, 2000.
[18] J.F. Guespin-Michel et al., "Epigenesis and Dynamic Similarity in Two Regulatory Networks in Pseudomonas Aeruginosa," Acta Biotheoretica, vol. 52, pp. 379-390, 2004.
[19] L. Calzone, F. Fages, and S. Soliman, "BIOCHAM: An Environment for Modeling Biological Systems and Formalizing Experimental Knowledge," Bioinformatics, vol. 22, no. 14, pp. 1805-1807, 2006.
[20] P.T. Monteiro et al., "Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks," Bioinformatics, vol. 24, no. 16, pp. 227-233, 2008.
[21] A. Rizk et al., "A General Computational Method for Robustness Analysis with Applications to Synthetic Gene Networks," Bioinformatics, vol. 25, no. 12, pp. i169-i178, 2009.
[22] R. Donaldson and D. Gilbert, "A Model Checking Approach to the Parameter Estimation of Biochemical Pathways," Proc. Int'l Conf. Computational Methods in Systems Biology, pp. 269-287, 2008.
[23] P. Collins et al., "Abstraction of Biochemical Reaction Systems on Polytopes," Proc. 18th IFAC World Congress, 2011.
[24] G. Batt et al., "Efficient Parameter Search for Qualitative Models of Regulatory Networks Using Symbolic Model Checking," technical report, INRIA, 2010.
[25] P. Ballarini et al., "Taming the Complexity of Biological Pathways through Parallel Computing," Briefings in Bioinformatics, vol. 10, no. 3, pp. 278-288, 2009.
[26] J. Barnat, L. Brim, and D. Šafránek, "High-Performance Analysis of Biological Systems Dynamics with the Divine Model Checker," Briefings in Bioinformatics, vol. 11, pp. 301-312, 2010.
[27] A. Donzé et al., "Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology," Proc. RECOMB'09, pp. 155-169, 2009.
[28] Z. Khalis et al., "The Smbionet Method for Discovering Models of Gene Regulatory Networks," Genes, Genomes and Genomics, vol. 3, no. 1, pp. 15-22, 2009.
[29] B. Pal et al., "BUSpec: A Framework for Generation of Verification Aids for Standard Bus Protocol Specifications," Integration, the VLSI J., vol. 40, no. 3, pp. 285-304, 2007.
[30] K. Hamaguchi et al., "Formal Verification of Speed-Dependent Asynchronous Circuits Using Symbolic Model Checking of Branching Time Regular Temporal Logic," Proc. Int'l Conf. Computer Aided Verification, pp. 410-420, 1991.
[31] C. Chaouiya et al., "Logical Modelling of Regulatory Networks with Ginsim 2.3," Biosystems, vol. 97, no. 2, pp. 134-139, 2009.
[32] G. Bernot et al., "Application of Formal Methods to Biological Regulatory Networks: Extending Thomas' Asynchronous Logical Approach with Temporal Logic," J. Theoretical Biology, vol. 229, no. 3, pp. 339-347, 2004.
[33] T. Mestl et al., "A Mathematical Framework for Describing and Analysing Gene Regulatory Networks," J. Theoretical Biology, vol. 176, no. 2, pp. 291-300, 1995.
[34] J. Barnat et al., "Parameter Scanning by Parallel Model Checking with Applications in Systems Biology," Proc. Ninth Int'l Workshop Parallel and Distributed Methods in Verification, and Second Int'l Workshop High Performance Computational Systems Biology (PDMC/HiBi '10), pp. 95-104, 2010.
[35] M. Swat, A. Kel, and H. Herzel, "Bifurcation Analysis of the Regulatory Modules of the Mammalian G1/S Transition," Bioinformatics, vol. 20, no. 10, pp. 1506-1511, 2004.
[36] S. Liang, S. Fuhrman, and R. Somogyi, "Reveal, A General Reverse Engineering Algorithm for Inference of Genetic Network Architectures," Proc. Pacific Symp. Biocomputing, vol. 29, no. 3, pp. 18-29, 1998.
[37] H. Ma, F. Boogerd, and I. Goryanin, "Modelling Nitrogen Assimilation of Escherichia Coli at Low Ammonium Concentration," J. Biotechnology, vol. 144, pp. 175-183, 2009.

Index Terms:
parallel processing,biology computing,formal verification,biological models,parameter synthesis,parallel model checking,computational system biology,biological systems dynamics,parameter uncertainty,Biological system modeling,Computational modeling,Algorithm design and analysis,Cost accounting,Kinetic theory,systems biology.,Biological networks,parallel model checking,dynamical systems,parameter synthesis
A. Streck, A. Krejci, L. Brim, J. Barnat, D. Safranek, M. Vejnar, T. Vejpustek, "On Parameter Synthesis by Parallel Model Checking," IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 9, no. 3, pp. 693-705, May-June 2012, doi:10.1109/TCBB.2011.110
Usage of this product signifies your acceptance of the Terms of Use.