An integrated modelling approach for R5-X4 mutation and HAART therapy assessment

We have modelled the within-patient evolutionary process during HIV infection using different methodologies. New viral strains arise during the course of HIV infection. These multiple strains of the virus are able to use different coreceptors, in particular the CCR5 and the CXCR4 (R5 and X4 phenotypes, respectively) influence the progression of the disease to the AIDS phase. We present a model of HIV early infection and CTLs response which describes the dynamics of R5 quasispecies, specifying the R5 to X4 switch and the effects of the immune response. We illustrate the dynamics of HIV multiple strains in the presence of multidrug HAART therapy. The HAART combined with X4 strain blocker drugs might help to reduce infectivity and lead to slower progression of the disease. On the methodology side, our model represents a paradigm of integrating formal methods and mathematical models as a general framework to study HIV multiple strains during disease progression, and it will inch towards providing help in selecting among vaccines and drug therapies. The results presented here are one of the rare cases of methodological cross comparison (stochastic and deterministic) and a novel implementation of model checking in therapy validation.