Share Email Print
cover

Proceedings Paper

Solving a discrete model of the lac operon using Z3
Format Member Price Non-Member Price
PDF $14.40 $18.00
cover GOOD NEWS! Your organization subscribes to the SPIE Digital Library. You may be able to download this paper for free. Check Access

Paper Abstract

A discrete model for the Lcac Operon is solved using the SMT-solver Z3. Traditionally the Lac Operon is formulated in a continuous math model. This model is a system of ordinary differential equations. Here, it was considerated as a discrete model, based on a Boolean red. The biological problem of Lac Operon is enunciated as a problem of Boolean satisfiability, and it is solved using an STM-solver named Z3. Z3 is a powerful solver that allows understanding the basic dynamic of the Lac Operon in an easier and more efficient way. The multi-stability of the Lac Operon can be easily computed with Z3. The code that solves the Boolean red can be written in Python language or SMT-Lib language. Both languages were used in local version of the program as online version of Z3. For future investigations it is proposed to solve the Boolean red of Lac Operon using others SMT-solvers as cvc4, alt-ergo, mathsat and yices.

Paper Details

Date Published: 22 May 2014
PDF: 11 pages
Proc. SPIE 9118, Independent Component Analyses, Compressive Sampling, Wavelets, Neural Net, Biosystems, and Nanoengineering XII, 911814 (22 May 2014); doi: 10.1117/12.2049755
Show Author Affiliations
Natalia A. Gutierrez, 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