The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - September/October (2011 vol.8)
pp: 1393-1399
Elena Dubrova , Royal Institute of Technology, Stockholm
Maxim Teslenko , Royal Institute of Technology, Stockholm
ABSTRACT
This paper addresses the problem of finding attractors in synchronous Boolean networks. The existing Boolean decision diagram-based algorithms have limited capacity due to the excessive memory requirements of decision diagrams. The simulation-based algorithms can be applied to larger networks, however, they are incomplete. We present an algorithm, which uses a SAT-based bounded model checking to find all attractors in a Boolean network. The efficiency of the presented algorithm is evaluated by analyzing seven networks models of real biological processes, as well as 150,000 randomly generated Boolean networks of sizes between 100 and 7,000. The results show that our approach has a potential to handle an order of magnitude larger models than currently possible.
INDEX TERMS
Bounded model checking, SAT, Boolean network, attractor, gene regulatory network.
CITATION
Elena Dubrova, Maxim Teslenko, "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks", IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol.8, no. 5, pp. 1393-1399, September/October 2011, doi:10.1109/TCBB.2010.20
REFERENCES
[1] B. Alberts, D. Bray, J. Lewis, M. Ra, K. Roberts, and J.D. Watson, Molecular Biology of the Cell. Garland Publishing, 1994.
[2] T. Schlitt and A. Brazma, “Current Approaches to Gene Regulatory Network Modelling,” BMC Bioinformatics, vol. 8, Suppl 6: S9, 2007.
[3] S.A. Kauffman, “Metabolic Stability and Epigenesis in Randomly Constructed Nets,” J. Theoretical Biology, vol. 22, pp. 437-467, 1969.
[4] S. Huang and D.E. Ingber, “Shape-Dependent Control of Cell Growth, Differentiation, and Apoptosis: Switching between Attractors in Cell Regulatory Networks,” Experimental Cell Research, vol. 26, no. 1, pp. 91-103, 2000.
[5] R. Albert and H.G. Othmer, “The Topology of the Regulatory Interactions Predicts the Expression Pattern of the Segment Polarity Genes in Drosophila Melanogaster,” J. Theoretical Biology, vol. 223, no. 1, pp. 1-18, 2003.
[6] M.I. Davidich and S. Bornholdt, “Boolean Network Model Predicts Cell Cycle Sequence of Fission Yeast,” PLoS ONE, vol. 3, no. 2, p. e1672, 2008.
[7] S.A. Kauffman and E.D. Weinberger, “The NK Model of Rugged Fitness Landscapes and Its Application to Maturation of the Immune Response,” J. Theoretical Biology, vol. 141, pp. 211-245, 1989.
[8] S. Bornholdt and T. Rohlf, “Topological Evolution of Dynamical Networks: Global Criticality from Local Dynamics,” Physical Rev. Letters, vol. 84, pp. 6114-6117, 2000.
[9] A. Chaos, M. Aldana, C. Espinosa-Soto, B. Leon, A. Arroyo, and E. Alvarez-Buylla, “From Genes to Flower Patterns and Evolution: Dynamic Models of Gene Regulatory Networks,” Plant Growth Regulation, vol. 25, no. 4, pp. 278-289, 2006.
[10] H. de Jong and M. Page, “Search for Steady States of Piecewise-Linear Differential Equation Models of Genetic Regulatory Networks,” IEEE/ACM Trans. Computational Biology and Bioinformatics, vol. 5, no. 2, pp. 208-222, Apr.-June 2008.
[11] A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. Design Automation Conf. (DAC '99), pp. 317-320, June 1999.
[12] G. Batt, D. Ropers, H. de Jong, J. Geiselmann, R. Mateescu, M. Page, and D. Schneider, “Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli,” Bioinformatics, vol. 21, no. 1, pp. 19-28, 2005.
[13] V. Mysore and B. Mishra, “Algorithmic Algebraic Model Checking IV: Characterization of Metabolic Networks,” Proc. Int'l Conf. Algebraic Biology (AB '07), pp. 170-184, July 2007.
[14] M. Calder, V. Vyshemirsky, D. Gilbert, and R. Orton, “Analysis of Signalling Pathways Using the PRISM Model Checker,” Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '05), pp. 179-190, Apr. 2005.
[15] D. Gilbert, M. Heiner, and S. Lehrack, “A Unifying Framework for Modelling and Analysing Biochemical Pathways Using Petri Nets,” Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '07), pp. 200-216, Sept. 2007.
[16] P. Ballarini, R. Mardare, and I. Mura, “Analysing Biochemical Oscillation through Probabilistic Model Checking,” Electronic Notes Theoretical Computer Science, vol. 229, no. 1, pp. 3-19, 2009.
[17] C.J. Langmead and S.K. Jha, “Symbolic Approaches for Finding Control Strategies in Boolean Networks,” Bioinformatics and Computational Biology, vol. 2, no. 7, pp. 323-338, 2009.
[18] R. Thomas and R. D'Ari, Biological Feedback. CRC Press, 1990.
[19] E. Dubrova, “Random Multiple-Valued Networks: Theory and Applications,” Proc. Int'l Symp. Multiple-Valued Logic (ISMVL '06), pp. 27-33, May 2006.
[20] A. Garg, L. Mendoza, I. Xenarios, and G. DeMicheli, “Modeling of Multiple Valued Gene Regulatory Networks,” Proc. 29th IEEE Int'l Conf. Eng. in Medicine and Biology Soc. (EMBC '07), pp. 1398-1404, Aug. 2007.
[21] E.M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman, “Completeness and Complexity of Bounded Model Checking,” Proc. Fifth Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI '04), pp. 85-96, Jan. 2004.
[22] J. Burch et al., “Symbolic Model Checking: 1020 States and Beyond,” Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 1-33, 1990.
[23] D. Kroening and O. Strichman, “Efficient Computation of Recurrence Diameters,” Proc. Fourth Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI '03), pp. 298-309, Jan. 2003.
[24] E. Dubrova, M. Teslenko, and A. Martinelli, “Kauffman Networks: Analysis and Applications,” Proc. IEEE/ACM Int'l Conf. Computer-Aided Design, pp. 479-484, Nov. 2005.
[25] S. Bilke and F. Sjunnesson, “Stability of the Kauffman Model,” Physical Rev. E, vol. 65, p. 016129, 2001.
[26] J.E.S. Socolar and S.A. Kauffman, “Scaling in Ordered and Critical Random Boolean Networks,” Physical Rev. Letters, vol. 90, no. 6, p. 068702, 2003.
[27] C. Oosawa, “Effects of Alternative Connectivity on Behavior of Randomly Constructed Boolean Networks,” Physica D: Nonlinear Phenomena, vol. 170, no. 2, pp. 143-161, 2002.
[28] L. Raeymaekers, “Dynamics of Boolean Networks Controlled by Biologically Meaningful Functions,” J. Theoretical Biology, vol. 218, no. 3, pp. 331-341, 2002.
[29] T. Akutsu, S. Kuhara, O. Maruyama, and S. Miyano, “A System for Identifying Genetic Networks from Gene Expression Patterns Produced by Gene Disruptions and Overexpressions,” Genome Informatics, vol. 9, pp. 151-160, 1998.
[30] T. Tamura and T. Akutsu, “An Improved Algorithm for Detecting a Singleton Attractor in a Boolean Network Consisting of AND/OR Nodes,” Proc. Third Int'l Conf. Algebraic Biology (AB '08), pp. 216-229, July/Aug. 2008.
[31] T. Akutsu and T. Tamura, “On Finding a Fixed Point in a Boolean Network with Maximum Indegree 2,” IEICE Trans. Fundamentals of Electronics, Comm. and Computer Sciences, vol. E92.A, no. 8, pp. 1771-1778, 2009.
[32] A. Naldi, D. Thieffry, and C. Chaouiya, “Decision Diagrams for the Representation and Analysis of Logical Models of Genetic Networks,” Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '07), pp. 233-247, Sept. 2007.
[33] R. Thomas, “Regulatory Networks Seen as Asynchronous Automata: A Logical Description,” J. Theoretical Biology, vol. 153, pp. 1-23, 1991.
[34] D.J. Irons, “Improving the Efficiency of Attractor Cycle Identification in Boolean Networks,” Physica D: Nonlinear Phenomena, vol. 217, pp. 7-21, 2006.
[35] E. Dubrova and M. Teslenko, “Kauffman Networks: From Nature to Electronics,” Proc. Notes of IEEE Int'l Workshop Logic Synthesis, pp. 56-60, June 2005.
[36] A. Garg, I. Xenarios, L. Mendoza, and G. De Micheli, “An Efficient Method for Dynamic Analysis of Gene Regulatory Networks and in Silico Gene Perturbation Experiments,” Proc. 11th Ann. Int'l Conf. Research in Computational Molecular Biology (RECOMB '07), pp. 62-76, Apr. 2007.
[37] G. Hasteer, A. Mathur, and P. Banerjee, “An Implicit Algorithm for Finding Steady States and Its Application to FSM Verification,” Proc. Design Automation Conf. (DAC '98), pp. 611-614, June 1998.
[38] A. Xie and P.A. Beerel, “Implicit Enumeration of Strongly Connected Components,” Proc. Int'l Conf. Computer-Aided Design (ICCAD '99), pp. 37-40, Nov. 1999.
[39] V. Devloo, P. Hansen, and M. Labb, “Identification of All Steady States in Large Biological Systems by Logical Analysis,” Bull. of Math. Biology, vol. 65, no. 6, pp. 1025-1051, 2003.
[40] L. Bordeaux, Y. Hamadi, and L. Zhang, “Propositional Satisfiability and Constraint Programming: A Comparative Survey,” ACM Computing Surveys, vol. 38, no. 4, p. 12, 2006.
[41] N. Een and N. Sorensson, “MiniSat—A SAT Solver with Conflict-Clause Minimization,” Proc. Int'l Conf. Theory and Applications of Satisfiability Testing (SAT '05), June 2005.
[42] F. Li, T. Long, Y. Lu, Q. Ouyang, and C. Tang, “The Yeast Cell-Cycle Network is Robustly Designed,” Proc. Nat'l Academy of Sciences USA, vol. 101, no. 14, pp. 4781-4786, 2004.
[43] A. Faure, A. Naldi, C. Chaouiya, and D. Thieffry, “Dynamical Analysis of a Generic Boolean Model for the Control of the Mammalian Cell Cycle,” Bioinformatics, vol. 22, pp. e124-e131(1), 2006.
[44] S. Klamt, J. Saez-Rodriguez, J.A. Lindquist, L. Simeoni, and E.D. Gilles, “A Methodology for the Structural and Functional Analysis of Signaling and Regulatory Networks,” BMC Bioinformatics, vol. 7, article no. 56, 2006.
[45] L. Mendoza and I. Xenarios, “A Method for the Generation of Standardized Qualitative Dynamical Systems of Regulatory Networks,” Theoretical Biology and Medical Modelling, vol. 3, no. 1, pp. 13-31, 2006.
[46] A. Garg, A. Di Cara, I. Xenarios, L. Mendoza, and G. De Micheli, “Synchronous Versus Asynchronous Modeling of Gene Regulatory Networks,” Bioinformatics, vol. 24, no. 17, pp. 1917-1925, 2008.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool