Abstract
The logical framework allows for the qualitative analysis of complex regulatory networks that control cellular processes. However, the study of large models is still hampered by the combinatorial explosion of the number of states. In this manuscript we present our work to analyse logical models of regulatory networks using model checking techniques.We propose a symbolic encoding (using NuSMV) of logical regulatory graphs, also considering priority classes. To achieve a reduction of the state space, we further label the transitions with the values of the input components. This encoding has been implemented in the form of an export facility in GINsim, a software dedicated to logical models. The potential of our symbolic encoding is illustrated through the analysis of the segment-polarity module of the Drosophila embryo segmentation.
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
Batt, G., Ropers, D., de Jong, H., Geiselmann, J., Mateescu, R., Page, M., Schneider, D.: Validation of qualitative models of genetic regulatory networks by model checking: Analysis of the nutritional stress response in Escherichia coli. Bioinformatics 21 (suppl.), i19–i28 (2005)
Bernot, G., Comet, J., Richard, A., Guespin, J.: Application of formal methods to biological regulatory networks: Extending Thomas’ asynchronous logical approach with temporal logic. J. Theor. Biol. 229(3), 339–348 (2004)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Fauré, A., Naldi, A., Chaouiya, C., Thieffry, D.: Dynamical analysis of a generic boolean model for the control of the mammalian cell cycle. Bioinformatics 22(14), 124–131 (2006)
Müller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)
Naldi, A., Berenguier, D., Fauré, A., Lopez, F., Thieffry, D., Chaouiya, C.: Logical modelling of regulatory networks with GINsim 2.3. Biosystems 97(2), 134–139 (2009)
Pecheur, C., Raimondi, F.: Symbolic Model Checking of Logics with Actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 113–128. Springer, Heidelberg (2007)
Sánchez, L., Chaouiya, C., Thieffry, D.: Segmenting the fly embryo: a logical analysis of the segment-polarity cross-regulatory module. Int. J. Dev. Biol. 52(8), 1059–1075 (2008)
Sánchez, L., Thieffry, D.: Segmenting the fly embryo: a logical analysis of the pair-rule cross-regulatory module. J. Theor. Biol. 224(4), 517–537 (2003)
Thomas, R., D’Ari, R.: Biological Feedback. CRC Press (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monteiro, P.T., Chaouiya, C. (2012). Efficient Verification for Logical Models of Regulatory Networks. In: Rocha, M., Luscombe, N., Fdez-Riverola, F., Rodríguez, J. (eds) 6th International Conference on Practical Applications of Computational Biology & Bioinformatics. Advances in Intelligent and Soft Computing, vol 154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28839-5_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-28839-5_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28838-8
Online ISBN: 978-3-642-28839-5
eBook Packages: EngineeringEngineering (R0)