Formal reasoning on qualitative models of coinfection of HIV and Tuberculosis and HAART therapy

Abstract

Background: Several diseases, many of which nowadays pandemic, consist of multifactorial pathologies. Paradigmatic examples come from the immune response to pathogens, in which cases the effects of different infections combine together, yielding complex mutual feedback, often a positive one that boosts infection progression in a scenario that can easily become lethal. HIV is one such infection, which weakens the immune system favouring the insurgence of opportunistic infections, amongst which Tuberculosis (TB). The treatment with antiretroviral therapies has shown effective in reducing mortality. An in-depth understanding of complex systems, like the one consisting of HIV, TB and related therapies, is an open great challenge, on the boundaries of bioinformatics, computational and systems biology.

Results: We present a simplified formalisation of the highly dynamic system consisting of HIV, TB and related therapies, at the cellular level. The progression of the disease (AIDS) depends hence on interactions between viruses, cells, chemokines, the high mutation rate of viruses, the immune response of individuals and the interaction between drugs and infection dynamics. We first discuss a deterministic model of dual infection (HIV and TB) which is able to capture the long-term dynamics of CD4 T cells, viruses and Tumour Necrosis Factor (TNF). We contrast this model with a stochastic approach which captures intrinsic fluctuations of the biological processes. Furthermore, we also integrate automated reasoning techniques, i.e. probabilistic model checking, in our formal analysis. Beyond numerical simulations, model checking allows general properties (effectiveness of anti-HIV therapies) to be verified against the models by means of an automated procedure. Our work stresses the growing importance and flexibility of model checking techniques in bioinformatics. In this paper we i) describe HIV as a complex case of infectious diseases; ii) provide a number of different formal descriptions that suitably account for aspects of interests; iii) suggest that the integration of different models together with automated reasoning techniques can improve the understanding of infections and therapies through formal analysis methodologies.

Conclusion: We argue that the described methodology suitably supports the study of viral infections in a formal, automated and expressive manner. We envisage a long-term contribution of this kind of approaches to clinical Bioinformatics and Translational Medicine.

Figure 1

The maximum likelihood phylogeny under the JTT model of evolution for a set of chemokine receptors amino acid sequences.

Figure 2

Viral load, CD4 T and TNF over the course of time. (a) Time evolution of viral load and CD4 where mutation of V5 leads to V4 at around day t = 900 and opportunistic diseases (TB) appears at around day t = 2900 (b) dynamics of viral load and TNF over time.

Figure 3

Experiments with HAART therapy. Therapy start from (a) day t = 250 to day t = 350 (b) day t = 950 to day t = 1050 (c) day t = 2250 to day t = 2350 and (d) day t = 3150 to day t = 3250.

Figure 4

A limited fragment of the time course of Viruses, CD4 T cells and TB bacteria in the case of (a) no treatment and (b) treatment with HAART.

Figure 5

The implementation of the stochastic model (Table 2) in the PRISM modelling language.