Share Email Print
cover

Proceedings Paper

Using computer algebra and SMT-solvers to analyze a mathematical model of cholera propagation
Author(s): Mariana Trujillo Arredondo
Format Member Price Non-Member Price
PDF $14.40 $18.00

Paper Abstract

We analyze a mathematical model for the transmission of cholera. The model is already defined and involves variables such as the pathogen agent, which in this case is the bacterium Vibrio cholera, and the human population. The human population is divided into three classes: susceptible, infectious and removed. Using Computer Algebra, specifically Maple we obtain two equilibrium states: the disease free state and the endemic state. Using Maple it is possible to prove that the disease free state is locally asymptotically stable if and only if R0 < 1. Using Maple it is possible to prove that the endemic equilibrium state is locally stable when it exists, it is to say when R0 > 1. Using the package Red-Log of the Computer algebra system Reduce and the SMT-Solver Z3Py it is possible to obtain numerical conditions for the model. The formula for the basic reproductive number makes a synthesis with all epidemic parameters in the model. Also it is possible to make numerical simulations which are very illustrative about the epidemic patters that are expected to be observed in real situations. We claim that these kinds of software are very useful in the analysis of epidemic models given that the symbolic computation provides algebraic formulas for the basic reproductive number and such algebraic formulas are very useful to derive control measures. For other side, computer algebra software is a powerful tool to make the stability analysis for epidemic models given that the all steps in the stability analysis can be made automatically: finding the equilibrium points, computing the jacobian, computing the characteristic polynomial for the jacobian, and applying the Routh-Hurwitz theorem to the characteristic polynomial. Finally, using SMT-Solvers is possible to make automatically checks of satisfiability, validity and quantifiers elimination being these computations very useful to analyse complicated epidemic models.

Paper Details

Date Published: 5 June 2014
PDF: 11 pages
Proc. SPIE 9112, Sensing Technologies for Global Health, Military Medicine, and Environmental Monitoring IV, 91121I (5 June 2014); doi: 10.1117/12.2048855
Show Author Affiliations
Mariana Trujillo Arredondo, Univ. EAFIT (Colombia)


Published in SPIE Proceedings Vol. 9112:
Sensing Technologies for Global Health, Military Medicine, and Environmental Monitoring IV
Šárka O. Southern; Mark A. Mentzer; Isaac Rodriguez-Chavez; Virginia E. Wotring, Editor(s)

© SPIE. Terms of Use
Back to Top