Abstract
Model checking has historically been an important tool to verify models of a wide variety of systems. Typically a model has to exhibit certain properties to be classed ‘acceptable’. In this work we use model checking in a new setting; parameter estimation. We characterise the desired behaviour of a model in a temporal logic property and alter the model to make it conform to the property (determined through model checking). We have implemented a computational system called MC2(GA) which pairs a model checker with a genetic algorithm. To drive parameter estimation, the fitness of set of parameters in a model is the inverse of the distance between its actual behaviour and the desired behaviour. The model checker used is the simulation-based Monte Carlo Model Checker for Probabilistic Linear-time Temporal Logic with numerical constraints, MC2(PLTLc). Numerical constraints as well as the overall probability of the behaviour expressed in temporal logic are used to minimise the behavioural distance. We define the theory underlying our parameter estimation approach in both the stochastic and continuous worlds. We apply our approach to biochemical systems and present an illustrative example where we estimate the kinetic rate constants in a continuous model of a signalling pathway.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Wolkenhauer, O.: Systems Biology: the Reincarnation of Systems Theory Applied in Biology? Briefings in Bioinformatics 2(3), 258–270 (2001)
Kolch, W., Calder, M., Gilbert, D.: When kinases meet mathematics: the systems biology of MAPK signalling. FEBS Lett. 579, 1891–1895 (2005)
Gilbert, D., Heiner, M., Lehrack, S.: A unifying framework for modelling and analysing biochemical pathways using Petri nets. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 200–216. Springer, Heidelberg (2007)
Vyshemirsky, V., Girolami, M.: Bayesian Ranking of Biochemical System Models. Bioinformatics 24(6), 833–839 (2008)
Maria, G.: A Review of Algorithms and Trends in Kinetic Model Identification for Chemical and Biochemical Systems. Chem. Biochem. Eng. Q. 18(3), 195–222 (2004)
Donaldson, R., Gilbert, D.: A Monte Carlo Model Checker for Probabilistic LTL with Numerical Constraints. Technical report, University of Glasgow, Department of Computing Science (2008)
Baier, C.: On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, University of Mannheim (1998)
Brightman, F., Fell, D.: Differential feedback regulation of the mapk cascade underlies the quantitative differences in egf and ngf signalling in pc12 cells. FEBS Lett. 482, 169–174 (2000)
Gilbert, D., Heiner, M., Rosser, S., Fulton, R., Gu, X., Trybilo, M.: A Case Study in Model-driven Synthetic Biology. In: Biologically Inspired Cooperative Computing: BICC 2008. IFIP, vol. 268, pp. 163–175. Springer, Heidelberg (2008)
Pnueli, A.: The Temporal Semantics of Concurrent Programs. Theor. Comput. Sci. 13, 45–60 (1981)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) (third printing, 2001)
Fages, F., Rizk, A.: On the Analysis of Numerical Data Time Series in Temporal Logic. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 48–63. Springer, Heidelberg (2007)
Hansson, H., Jonsson, B.: A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying Continuous-Time Markov Chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Goldberg, D.E.: Genetic Algorithms in Search, Optimization and Machine Learning. Addison-Wesley Longman Publishing Co., Inc., Boston (1989)
BioNessie: A Biochemical Pathway Simulation and Analysis Tool. University of Glasgow, http://www.bionessie.org
MC2(PLTLc) Website: MC2(PLTLc) - PLTLc model checker. University of Glasgow (2008), http://www.brc.dcs.gla.ac.uk/software/mc2/
Meffert, K., et al.: JGAP - Java Genetic Algorithms and Genetic Programming Package (2008), http://jgap.sf.net/
Hucka, M., Finney, A., Sauro, H.M., Bolouri, H., Doyle, J.C., Kitano, H., et al.: The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models. J. Bioinformatics 19, 524–531 (2003)
Fujarewicz, K., Kimmel, M., Lipniacki, T., Świerniak, A.: Parameter estimation for models of cell signaling pathways based on semi-quantitative data. In: BioMed 2006: Proceedings of the 24th IASTED international conference on Biomedical engineering, Anaheim, CA, USA, pp. 306–310. ACTA Press (2006)
Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine Learning Biochemical Networks from Temporal Logic Properties. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 68–94. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Donaldson, R., Gilbert, D. (2008). A Model Checking Approach to the Parameter Estimation of Biochemical Pathways. In: Heiner, M., Uhrmacher, A.M. (eds) Computational Methods in Systems Biology. CMSB 2008. Lecture Notes in Computer Science(), vol 5307. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88562-7_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-88562-7_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88561-0
Online ISBN: 978-3-540-88562-7
eBook Packages: Computer ScienceComputer Science (R0)