Share Email Print
cover

Proceedings Paper

Analyzing toys models of Arabidopsis and Drosphila using Z3 SMT-LIB
Format Member Price Non-Member Price
PDF $14.40 $18.00

Paper Abstract

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.

Paper Details

Date Published: 22 May 2014
PDF: 15 pages
Proc. SPIE 9118, Independent Component Analyses, Compressive Sampling, Wavelets, Neural Net, Biosystems, and Nanoengineering XII, 911813 (22 May 2014); doi: 10.1117/12.2050071
Show Author Affiliations
Martín Rodríguez Vega, Univ. EAFIT (Colombia)


Published in SPIE Proceedings Vol. 9118:
Independent Component Analyses, Compressive Sampling, Wavelets, Neural Net, Biosystems, and Nanoengineering XII
Harold H. Szu; Liyi Dai, Editor(s)

© SPIE. Terms of Use
Back to Top