Toy models for the Arabidopsis Thaliana flower and the Drosophila are analyzed using Microsoft SMT-Solver Z3 with the SMT-LIB language. The models are formulated as Boolean networks which describe the metabolic cycles for Arabidopsis and Drosophila. The dynamic activation of the different bio macromolecules is described by the variables and laws of Boolean transition. Specifically, bitvectors and assertions, which describe the change of state of bitvectors from a sampling time to the next, are used. The dynamic feasibility problem of the biological network is translated to a Boolean satisfiability problem. The corresponding dynamic attractors are represented as a model of satisfiability. The Z3 software allows all required computations in a friendly and efficient manner. It is expected that the SMT-solvers, such as Z3, will become a routine tool in system biology and that they will provide bio-nanosystem design techniques. As a line for future research, the study of the models for Arabidopsis and Drosophila using different SMT-solvers such as CVC4, Mathsat and Yices, is proposed.
Tópico:
Gene Regulatory Network Analysis
Citaciones:
4
Citaciones por año:
Altmétricas:
0
Información de la Fuente:
FuenteProceedings of SPIE, the International Society for Optical Engineering/Proceedings of SPIE