Abstract
The Wnt/β-catenin signalling pathway plays an important role in the proliferation of neural cells, and hence it is the main focus of several research aimed at understanding neurodegenerative pathologies. In this paper we consider a compact model of the basic mechanisms of the Wnt/β-catenin pathway and we analyse its dynamics by application of an expressive temporal logic formalism, namely the Hybrid Automata Stochastic Logic. This allows us to formally characterise, and effectively assess, sophisticated aspects of the Wnt/β-catenin pathway dynamics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for CTMCs. IEEE Trans. on Software Eng. 29(6) (2003)
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST 2011), pp. 143–144. IEEE Computer Society Press (September 2011)
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Proc. Valuetools (2011)
Ballarini, P., Mäkelä, J., Ribeiro, A.S.: Expressive statistical model checking of genetic networks with delayed stochastic dynamics. In: Gilbert, D., Heiner, M. (eds.) CMSB 2012. LNCS, vol. 7605, pp. 29–48. Springer, Heidelberg (2012)
Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: A flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013)
Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of CTMC against timed automata specifications. In: Proc. LICS 2009 (2009)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 388–404. Springer, Heidelberg (2012)
Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL TA. IEEE Trans. on Software Eng. 35 (2009)
Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theoretical Computer Science 319(3), 239–257 (2008)
Kitano, H.: Foundations of Systems Biology. MIT Press (2002)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Legay, A., Delahaye, B.: Statistical model checking: An overview. CoRR, abs/1005.1327 (2010)
Mazemondet, O., Hubner, R., Frahm, J., Koczan, D., Bader, B.M., Weiss, D.G., Uhrmacher, A.M., Frech, M.J., Rolfs, A., Luo, J.: Quantitative and kinetic profile of wnt/β-catenin signaling components during human neural progenitor cell differentiation. Cell. Mol. Biol. Lett. (2011)
Mazemondet, O., John, M., Leye, S., Rolfs, A., Uhrmacher, A.M.: Elucidating the sources of β-catenin dynamics in human neural progenitor cells. PLOS-One 7(8), 1–12 (2012)
Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proc. QEST 2005 (2005)
Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ballarini, P., Gallet, E., Le Gall, P., Manceny, M. (2014). Formal Analysis of the Wnt/β-catenin through Statistical Model Checking. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014. Lecture Notes in Computer Science, vol 8803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45231-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-662-45231-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45230-1
Online ISBN: 978-3-662-45231-8
eBook Packages: Computer ScienceComputer Science (R0)