A model to determinate the reproductive basic number, detonated Ro, for the case of population with heterogeneity in sexual activity and proportionate mixing is solved using computer algebra and SMT solvers. Specifically Maple and Z3 were used. The code for the solution of the model was written in Z3-Python, but it can also be played by Z3-SMT-Lib. Ro represents an algebraic synthesis of every epidemiological parameter. Numerical simulations were done to prove the effectiveness of the model and the code. The algebraic structure of Ro suggests the possible control measurements that should be implemented to avoid the propagation of the sexual transmitted diseases. The obtained results are important on the computational epidemiology field. As a future investigation, it is suggested to apply the STM solvers to analyze models for other kinds of epidemic diseases.
The diffusion rate of a spherical drug delivery device was analyzed using a Laplace transform-based method. The three-dimensional model represented a pharmaceutical agent distributed, not uniformly, in a polymeric matrix. Molecules
could only be transferred to the outside of the matrix through a thin spherical sector of the device. A closed-form
solution was obtained to help study the effects of diffusivity parameters and geometries on the cumulative amount of
drug released. The latter variable increased with the mass transfer and diffusion function and decreased with any
increment in the device’s length. The solution obtained was in terms of the Legendre polynoms, and developed using the
Maple software. It is expected that the results presented help to the future design of devices in pharmaceutical
engineering.
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.
Access to the requested content is limited to institutions that have purchased or subscribe to SPIE eBooks.
You are receiving this notice because your organization may not have SPIE eBooks access.*
*Shibboleth/Open Athens users─please
sign in
to access your institution's subscriptions.
To obtain this item, you may purchase the complete book in print or electronic format on
SPIE.org.
INSTITUTIONAL Select your institution to access the SPIE Digital Library.
PERSONAL Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.