Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-24T21:55:11.687Z Has data issue: false hasContentIssue false
  • English
  • Français

Static analysis of Biological Regulatory Networks dynamics using abstract interpretation

Published online by Cambridge University Press:  08 May 2012

LOÏC PAULEVÉ ,
MORGAN MAGNIN  and
OLIVIER ROUX
LOÏC PAULEVÉ
Affiliation:
LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), 1 rue de la Noë - B.P. 92101 - 44321 Nantes Cedex 3, France and LIX, École Polytechnique, 91128 Palaiseau Cedex, France Email: [email protected]
MORGAN MAGNIN
Affiliation:
LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), 1 rue de la Noë - B.P. 92101 - 44321 Nantes Cedex 3, France Email: [email protected]; [email protected]
OLIVIER ROUX
Affiliation:
LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), 1 rue de la Noë - B.P. 92101 - 44321 Nantes Cedex 3, France Email: [email protected]; [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The analysis of the dynamics of Biological Regulatory Networks (BRNs) requires innovative methods to cope with the state-space explosion. This paper settles an original approach for deciding reachability properties based on Process Hitting, which is a framework suitable for modelling dynamical complex systems. In particular, Process Hitting has been shown to be of interest in providing compact models of the dynamics of BRNs with discrete values. Process Hitting splits a finite number of processes into so-called sorts and describes the way each process is able to act upon (that is, to ‘hit’) another one (or itself) in order to ‘bounce’ it as another process of the same sort with further actions.

By using complementary abstract interpretations of the succession of actions in Process Hitting, we build a very efficient static analysis to over- and under-approximate reachability properties, which avoids the need to build the underlying states graph. The analysis is proved to have a low theoretical complexity, in particular when the number of processes per sorts is limited, while a very large number of sorts can be managed.

This makes such an approach very promising for the scalable analysis of abstract complex systems. We illustrate this through the analysis of a large BRN of 94 components. Our method replies quasi-instantaneously to reachability questions, while standard model-checking techniques regularly fail because of the combinatoric explosion of behaviours.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 22 , Issue 4 , August 2012 , pp. 651 - 685
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alimonti, P., Feuerstein, E., Laura, L. and Nanni, U. (2011) Linear time analysis of properties of conflict-free and general petri nets. Theoretical Computer Science 412 (4–5)320–338.CrossRefGoogle Scholar
Aracena, J. (2008) Maximum number of fixed points in regulatory boolean networks. Bulletin of Mathematical Biology 70 (5)1398–1409.CrossRefGoogle ScholarPubMed
Bernot, G., Cassez, F., Comet, J.-P., Delaplace, F., Müller, C. and Roux, O. (2007) Semantics of biological regulatory networks. Electronic Notes in Theoretical Computer Science 180 (3)3–14.CrossRefGoogle Scholar
Bernot, G., Comet, J.-P. and Khalis, Z. (2008) Gene regulatory networks with multiplexes. European Simulation and Modelling Conference Proceedings 423–432.Google Scholar
Brand, D. and Zafiropulo, P. (1983) On communicating finite-state machines. Journal of the ACM 30 323–342.CrossRefGoogle Scholar
Clarke, E. M. and Emerson, E. A. (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. Springer-Verlag Lecture Notes in Computer Science 131 52–71.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages – POPL '77 238–252.CrossRefGoogle Scholar
Cousot, P. and Cousot, R. (1992) Abstract interpretation frameworks. Journal of Logic and Computation 2 (4)511–547.CrossRefGoogle Scholar
Danos, V., Feret, J., Fontana, W. and Krivine, J. (2008) Abstract interpretation of cellular signalling networks. In: Logozzo, F., Peled, D. and Zuck, L. (eds.) Verification, Model Checking, and Abstract Interpretation. Springer-Verlag Lecture Notes in Computer Science 4905 83–97.CrossRefGoogle Scholar
Hamez, A., Thierry-Mieg, Y. and Kordon, F. (2009) Building efficient model checkers using hierarchical set decision diagrams and automatic saturation. Fundamenta Informaticae 94 (3–4)413–437.CrossRefGoogle Scholar
Klamt, S., Saez-Rodriguez, J., Lindquist, J., Simeoni, L. and Gilles, E. (2006) A methodology for the structural and functional analysis of signaling and regulatory networks. BMC Bioinformatics 7 (1)56.CrossRefGoogle ScholarPubMed
Paulevé, L., Magnin, M. and Roux, O. (2011a) Abstract Interpretation of Dynamics of Biological Regulatory Networks. In: Proceedings of The First International Workshop on Static Analysis and Systems Biology (SASB 2010). Electronic Notes in Theoretical Computer Science 272 43–56.CrossRefGoogle Scholar
Paulevé, L., Magnin, M. and Roux, O. (2011b) Refining dynamics of gene regulatory networks in a stochastic π-calculus framework. In: Priami, C., Back, R.-J., Petre, I. and de Vink, E. (eds.) Transactions on Computational Systems Biology XIII. Springer-Verlag Lecture Notes in Computer Science 6575 171–191.CrossRefGoogle Scholar
Paulevé, L. and Richard, A. (2010) Topological Fixed Points in Boolean Networks. Comptes Rendus de l'Académie des Sciences - Series I - Mathematics 348 (15–16)825–828.Google Scholar
Pilegaard, H., Nielson, F. and Nielson, H. R. (2005) Static analysis of a model of the LDL degradation pathway. In: Plotkin, G. (ed.) Third International Workshop on Computational Methods in Systems Biology (CMSB'05), University of Edinburgh.Google Scholar
Remy, É., Ruet, P. and Thieffry, D. (2008) Graphic requirements for multistability and attractive cycles in a boolean dynamical framework. Advances in Applied Mathematics 41 (3)335–350.CrossRefGoogle Scholar
Richard, A. (2010) Negative circuits and sustained oscillations in asynchronous automata networks. Advances in Applied Mathematics 44 (4)378–392.CrossRefGoogle Scholar
Richard, A. and Comet, J.-P. (2007) Necessary conditions for multistationarity in discrete dynamical systems. Discrete Applied Mathematics 155 (18)2403–2413.CrossRefGoogle Scholar
Richard, A., Comet, J.-P. and Bernot, G. (2006) Formal Methods for Modeling Biological Regulatory Networks. In: Gabbar, H. A. (ed.) Modern Formal Methods and Applications, Springer-Verlag 83–122.CrossRefGoogle Scholar
Saez-Rodriguez, J. et al. (2007) A logical model provides insights into t cell receptor signaling. PLoS Comput Biol 3 (8)e163.CrossRefGoogle ScholarPubMed
Thomas, R. (1973) Boolean formalization of genetic control circuits. Journal of Theoretical Biology 42 (3)563–585.CrossRefGoogle ScholarPubMed