Abstract
We present a computational method in which modular and Groebner bases (GB) computation in Boolean rings are used for solving problems in Boolean gene regulatory networks (BN). In contrast to other known algebraic approaches, the degree of intermediate polynomials during the calculation of Groebner bases using our method will never grow resulting in a significant improvement in running time and memory space consumption. We also show how calculation in temporal logic for model checking can be done by means of our direct and efficient Groebner basis computation in Boolean rings. We present our experimental results in finding attractors and control strategies of Boolean networks to illustrate our theoretical arguments. The results are promising. Our algebraic approach is more efficient than the state-of-the-art model checker NuSMV on BNs. More importantly, our approach finds all solutions for the BN problems.
A preliminary version of this paper appeared in BIOCOMP’09
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
References
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of Design Automation Conference (DAC’99), 1999
P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessor using satisfiability solvers. In Proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, volume 2102 of LNCS, pages 454–464, Paris, France. Springer, 2001
R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992
B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-dimensional Polynomial Ideal (in German). PhD thesis, Institute of Mathematics, University of Innsbruck, Innsbruck, Austria, 1965
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT, 1999
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994
E. Dubrova, M. Teslenko, and A. Martinelli. Kauffman networks: analysis and applications. In ICCAD ’05: Proceedings of the 2005 IEEE/ACM International Conference on Computer-Aided Design, pages 479–484, Washington, DC, USA. IEEE, 2005
G. Hermann. Die Frage der endlich vielen Schritte in der Theorie der Polynomideale. Mathematische Annalen, 95:736–788, 1925
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1–33, Washington, DC, USA. IEEE, 1990
O. Kupferman and M. Vardi. From complementation to certification. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 591–606. Springer, 2004
R. Laubenbacher and B. Stigler. A computational algebra approach to the reverse-engineering of gene regulatory networks. Journal of Theoretical Biology, 229:523–537, 2004
K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993
A. Pnueli. The temporal logic of programs. In Proceedings of 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977
Q.-N. Tran. Groebner bases computation in boolean rings is P-SPACE. International Journal of Applied Mathematics and Computer Sciences, 5(2):109–114
Q.-N. Tran and M. Y. Vardi. Groebner bases computation in Boolean rings for symbolic model checking. In Proceedings of IASTED 2007 Conference on Modeling and Simulation, Montreal, Canada, 2007
A. Valmari. The state explosion problem. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of LNCS, pages 429–528. Springer, 1998
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Tran, QN. (2011). Algebraic Model Checking for Boolean Gene Regulatory Networks. In: Arabnia, H., Tran, QN. (eds) Software Tools and Algorithms for Biological Systems. Advances in Experimental Medicine and Biology, vol 696. Springer, New York, NY. https://doi.org/10.1007/978-1-4419-7046-6_12
Download citation
DOI: https://doi.org/10.1007/978-1-4419-7046-6_12
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-7045-9
Online ISBN: 978-1-4419-7046-6
eBook Packages: Biomedical and Life SciencesBiomedical and Life Sciences (R0)