Special Issue: The Sixth Asia-Pacific Bioinformatics Conference (APBC 2008); Guest Editor: Alvis Brazma, Satoru Miyano and Tatsuya AkutsuNo Access

SYMBOLIC APPROACHES FOR FINDING CONTROL STRATEGIES IN BOOLEAN NETWORKS

CHRISTOPHER JAMES LANGMEAD

Department of Computer Science and the Lane Centre for Computational Biology, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA 15213, USA

Corresponding author.

Search for more papers by this author

and

SUMIT KUMAR JHA

Department of Computer Science and the Lane Centre for Computational Biology, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA 15213, USA

Search for more papers by this author

https://doi.org/10.1142/S0219720009004084Cited by:46 (Source: Crossref)

Abstract

We present an exact algorithm, based on techniques from the field of Model Checking, for finding control policies for Boolean Networks (BN) with control nodes. Given a BN, a set of starting states, I, a set of goal states, F, and a target time, t, our algorithm automatically finds a sequence of control signals that deterministically drives the BN from I to F at, or before time t, or else guarantees that no such policy exists. Despite recent hardness-results for finding control policies for BNs, we show that, in practice, our algorithm runs in seconds to minutes on over 13,400 BNs of varying sizes and topologies, including a BN model of embryogenesis in Drosophila melanogaster with 15,360 Boolean variables. We then extend our method to automatically identify a set of Boolean transfer functions that reproduce the qualitative behavior of gene regulatory networks. Specifically, we automatically learn a BN model of D. melanogaster embryogenesis in 5.3 seconds, from a space containing 6.9 × 10¹⁰ possible models.

Keywords:

References

T. Akutsuet al., J. Theor. Biol. 244, 670 (2007), DOI: 10.1016/j.jtbi.2006.09.023. Crossref, Medline, Google Scholar
E. M. Clarke , O. Grumberg and D. A. Peled , Model Checking ( MIT Press , Cambridge , 1999 ) . Google Scholar
J. R. Burchet al., Symbolic model checking: 1020 states and beyond, Proc Fifth Ann IEEE Symposium on Logic in Computer Science (1990) pp. 428–439. Google Scholar
J. R. Burchet al., IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 3(4), 401 (1993). Google Scholar
A. Biereet al., Symbolic model checking using SAT procedures instead of BDDs, Proc 36th ACM/IEEE Conf on Design Automation (DAC) (1999) pp. 317–320. Google Scholar
A. Pnueli, The temporal logic of programs, Proc 18th IEEE Foundations of Computer Science (FOCS) (1977) pp. 46–57. Google Scholar
E. M. Clarkeet al., Int. J. of Found. of Comp. Sci. 14(4), 583 (2003), DOI: 10.1142/S012905410300190X. Link, Google Scholar
A. Cimattiet al., Nusmv 2: An opensource tool for symbolic model checking, Proc 14th International Conference on Computer Aided Verification (CAV02) (2002) pp. 359–364. Google Scholar
T. Akutsu, S. Miyano and S. Kuhara, Bioinformatics 16(8), 727 (2000), DOI: 10.1093/bioinformatics/16.8.727. Crossref, Medline, Google Scholar
R. Albert and H. G. Othmer, J. Theor. Biol. 223, 1 (2003), DOI: 10.1016/S0022-5193(03)00035-3. Crossref, Medline, Google Scholar
S. E. Harriset al., Complex 7(4), 23 (2002), DOI: 10.1002/cplx.10022. Crossref, Google Scholar
S. A. Kauffman , The Origins of Order: Self-Organization and Selection in Evolution ( Oxford University Press , 1993 ) . Crossref, Google Scholar
P. C. Chen and J. W. Chen, Biosystems 90(2), 535 (2007), DOI: 10.1016/j.biosystems.2006.12.005. Crossref, Medline, Google Scholar
A. Dattaet al., Mach. Learn. 52(2), 169 (2003), DOI: 10.1023/A:1023909812213. Crossref, Google Scholar
M. Antoniottiet al., Cell. Biochem. Biophys. 38(3), 271 (2003), DOI: 10.1385/CBB:38:3:271. Crossref, Medline, Google Scholar
N. Chabrier and F. Fages, Symbolic model checking of biochemical networks, Proc 1st Internl Workshop on Computational Methods in Systems Biology (2003) pp. 149–162. Google Scholar
E. M. Clarkeet al., Statistical model checking in biolab: Application to the automated analysis of the t-cell receptor signalling pathway, Proc 6th Conf on Computational Methods in Systems Biology, (CMSB) (2008) pp. 231–250. Google Scholar
M. Kwiatkowskaet al., Simulation and verification for computational modelling of signalling pathways, Proc 38th Conf on Winter simulation (WSC) (2006) pp. 1666–1674. Google Scholar
C. J. Langmead and S. K. Jha, Predicting protein folding kinetics via model checking, Lecture Notes in Bioinformatics: The 7th Workshop on Algorithms in Bioinformatics (WABI) (2007) pp. 252–264. Google Scholar
C. J. Langmead and S. K. Jha , Using bit vector decision procedures for analysis of protein folding pathways , Proc 4th Workshop on Constraints in Formal Verification (CFV) ( 2007 ) . Google Scholar
D. Nam, S. Seo and S. Kim, Mach. Learn. 65(1), 229 (2006), DOI: 10.1007/s10994-006-9014-z. Crossref, Google Scholar
T. Tabata, S. Eaton and T. B. Kornberg, Genes. Dev. 6(12B), 2635 (1992), DOI: 10.1101/gad.6.12b.2635. Crossref, Medline, Google Scholar
I. Shmulevichet al., Proc. Natl. Acad. Sci. USA. 100(19), 10734 (2003), DOI: 10.1073/pnas.1534782100. Crossref, Medline, Google Scholar
Langmead CJ, Towards inference and learning in dynamic bayesian networks using generalized evidence, Technical Report CMU-CS-08-151, Carnegie Mellon University, Department of Computer Science, 2008 . Google Scholar
O. Grumberg, A. Schuster and A. Yadgar, Memory efficient all-solutions sat solver and its application for reachability analysis, Proc 5th Int Conf on Formal Methods in Computer-Aided Design (FMCAD) (2004) pp. 275–289. Google Scholar
I. Zinovik, D. Kroening and Y. Chebiryak, An algebraic algorithm for the identification of Glass networks with periodic orbits along cyclic attractors, Proc 2nd Conf on Algebraic Biology (AB07) (2007) pp. 140–154. Google Scholar