Sorathiya, Anil 1 Bracciali, Andrea 2 Liò, Pietro 1
[1 ] Computer Laboratory, Cambridge University, William Gates Building,15 JJ Thomson Avenue, Cambridge CB3 0FD, UK
[2 ] Computer Science Department, University of Pisa, Largo Bruno Pontecorvo, 3, Pisa 56127, ITALY
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 indepth 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.
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 longterm 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 antiHIV 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.
We argue that the described methodology suitably supports the study of viral infections in a formal, automated and expressive manner. We envisage a longterm contribution of this kind of approaches to clinical Bioinformatics and Translational Medicine.
Human diseases result from abnormalities in an extremely complex system of molecular processes that are often caused by viral or bacterial infections. In these pathological processes, virtually no molecular entity acts in isolation and complexity is caused by the vast amount of dependencies between molecular and phenotype features. The key player of the human survival is the immune system which is a complex system that can be described as a large network of dynamical agents (cells and signalling molecules). A great challenge for contemporary molecular medicine is the modelling, description and ultimately the comprehension of the multistep and multiscale nature of the immune response to pathogens. An even greater challenge is when viral and bacterial infections occur together in the same patient. TB, which is caused by Mycobacterium tuberculosis, is the most frequent coinfection in patients infected by the human immunodeficiency virus type 1 (HIV1). TB makes more complicated the development of effective therapies.
Efforts for gaining further insights into the pathological mechanisms and novel therapeutic targets benefit from the integration of genomic, proteomic, metabolomic and environmental information. In this work we follow an integrated approach that relies on several sources, such as phylogeny information, traditionally explored within Bioinformatics, differential equations and stochastic modelling, both largely used in Systems Biology, and a formal reasoning technique, viz. Model Checking, developed in Theoretical Computer Science to assess properties of complex computational systems. Furthermore, the Bioinformatics approach in the study of viral dynamics has also focused on identifying variable regions in genomes and pathogenic islands in bacteria [ 1]. These integrated frameworks appear to be effective for the research in the biomedical problems.
Mathematical and computer science approaches have shown to be more effective in dissecting the network connectivity of cellular circuits and the corresponding dynamical characteristics. The mathematical description of the variation of biomolecular concentrations as a set of ODEs offers quantitative basis for predicting the behaviour and evolution of the system and for testing nonlinearities. An alternative approach is to use stochastic simulation via the Gillespie algorithm which provides an exact algorithmic solution of a set of reactions and a meaningful way to consider the noise [ 2]. The use of mathematical models in immunology has been very successful and has represented an insightful and essential complement to in vivo and in vitro experimental design and interpretation. Kinetic Model suggests that HIV1 in vivo is continuous and highly productive and that leads CD4 T cells count low [ 3]. Nowak and May has proposed a simple model on HIV dynamics by considering population of noninfected T cells, infected T cells and viral population [ 4]. Perelson has proposed mathematical models on interaction of HIV virus and T cells dynamic by considering one more variable (uninfectious viruses) [ 5]. The HIV quasispecies models have been inspired from the molecular quasispecies model in chemistry [ 6, 7]. Indeed mathematical models of HIV dynamics have proven valuable in understanding the mechanisms of many of the observed features of the progression of the HIV infection, see for example [ 3, 6 13]. In this paper we model coinfection of HIV and TB and the effect of HAART therapy on the model dynamics.
Recently, the observation that biological systems often exhibit interactive and concurrent behavior, similarly to computational concurrent systems, has led to the adoption of formal methods originally developed for the description and analysis of complex software systems in computer science. This abstraction "cell as computation", similar to the "DNA as string" and "protein as labeled graph" abstractions which have originated bioinformatics, has inspired the adoption of model checking methodologies to validate biological complex systems [ 14]. The growing success of model checking (see for instance [ 15 18]) relies in the specification of a biological property of interest which is expressed in a formal language, typically a formula of a suitable logic, and its verification is carried out by a fully automated procedure that returns either a positive response or a counter example [ 19].
The aim of this paper is to pipeline bioinformatics and quantitative models of infectious processes and antiHIV therapies, and then show how model checking techniques can contribute to the interpretation of the insilico results obtained from quantitative models of infectious diseases dynamics. Given that viral infections and the functioning of therapies often present stochastic aspects, we introduce a succinct but descriptive stochastic model of HIV infection associated with TB opportunistic infection. Then we extend it by modelling (the effects of) HAART antiHIV therapy. These models have then been implemented in PRISM, a state of the art probabilistic model checker supporting a logical language [ 20]. We illustrate, by means of two simple properties, the flavour of the verification made possible by these techniques and how this can contribute to a precise assessment of the information conveyed by the mathematical models.
Human immunodeficiency virus type 1 (HIV1) infection is characterised by the progressive loss of CD4 T cells. AntiHIV therapies act to eradicate or lower the concentration of the virus from the body and replenish the CD4 T cells reservoir. Infection by most strains of HIV requires interaction with CD4 T cells and a chemokine receptor, either CXCR4 or CCR5. Viral strains often use CCR5 during early stages of HIV1 and then switches to CXCR4 to enter into the cells. This switch emerges in more than 50% of patients [ 21, 22] and it has been linked with progression to AIDS because of an increased virulence through the formation of cell syncytia and the stimulation of the cellular factor called Tumour Necrosis Factor (TNF) which inhibits the replication of R5 HIV strains while has no effect on X4 HIV [ 23, 24].
It takes on an average 10 years to get infected by AIDS after having HIV infection. Some patients died within 2 years after getting infected by HIV, while others remained free of AIDS for more than 15 years. The withinpatient evolutionary process of viral sequence mutations during HIV infection has suggested improvements in antiHIV therapies. AntiHIV drugs are most effective when taken in a combination of three or more at the same time. This is called combination therapy or HAART (Highly Active Antiretroviral Therapy). Physicians recommend starting the therapies if you are ill because of HIV, or if your CD4 T cells count if low (below 200 cells per microL). HAART combinations usually include two drugs that are nucleoside analogues, and one protease inhibitor. The nucleoside analogues drugs result in targeting the viral reverse transcriptase which codes the viral RNA into the DNA that can be integrated into human cells, so transforming the cell into a factory for building blocks of the virus. The protease inhibitor acts as preventing an infected cell from producing new infectious virus particles.
Chemokines provide the key link between HIV and TB infection. Resistance to HIV infection has been found to be related to the following mutations. Delta32 CCR5, 190G CCR2 and 744A CX3CR1 and CCL3L1 [ 25]. The chemokine receptor CXCR3 can exhibit weak coreceptor function for several human immunodeficiency virus, both HIV1 and HIV2 strains and clinical isolates [ 26]. Gene expression data analysis of HIV infected macrophages showed large changes in betachemokines and RANTES (CCL5) [ 27]. The TB infection is known to produce larger effects than HIV infection on the chemokine networks. TB is associated with excess monocyte chemoattractant protein (MCP)1 and Tumour Necrosis Factor (TNF)alpha activity in situ, both are implicated in transcriptional activation of HIV1 [ 28]. It is also important to mention significant elevation of the chemokines CCL3, CCL4 and CCL8 [ 29]. Gene expression data analysis of TB infected macrophages versus uninfected, showed upregulation of the following genes. interleukin1 beta and interleukin8, macrophage inflammatory protein1 alpha, growthrelated oncogenebeta, epithelial cellderived neutrophilactivating peptide78, macrophagederived chemokine [ 30]. The most important mechanism through which TB enhances HIV1 replication and the progression to AIDS in dually infected patients is the augmentation in expression of TNFalpha and the HIV1 noninhibitory betachemokine (MCP1), low presence of HIV1 inhibitory betachemokines (MIP1 alpha, MIP1 beta, and RANTES). We have collected a set of human aminoacid sequences of all the chemokine receptors known to chemokines involved in HIV and tuberculosis and a set of control chemokine receptors. We have built a phylogenetic tree that describes the statistical relationship between those chemokine receptors (see Figure 1). The tree was generated using maximum likelihood on an alignment of the sequences of the external regions of the protein loops. In violet the chemokines receptors disrupted by both TB and HIV; in red those disrupted by HIV. Note that the switch between CCR5 and CXCR4 may involve other chemokine receptors. This may suggest to concentrate some efforts on therapies by intervening by blocking other chemokine receptors disfunction.
The disruption caused by the dual infection (HIV and TB) focuses on RANTES which blocks CCR5 and whose expression is upregulated by TNF. Therefore we incorporated TNF in our deterministic model to predict the potential effect of HAART on coinfection of HIV and TB. That evidence would explain the increase in CXCR4 usage with the increase of TNF concentration [ 31]. The relationship between HIV and TB seems to be very profound since quasispecies of both HIV and TB influence each other differently [ 32, 33]. Our phylogenetic results suggest that both diseases act synergically and not simply additively to alter the chemokine network.
Although differential equation models have long been used for the immune system and viral infection modelling, they focus on the average behavior of large populations of perfectly mixed, identical individuals. An improved realism is perhaps provided by stochastic simulations, which however are computationally intensive. Given that differential equations and stochastic descriptions have important pros and cons and a good degree of complementarity, a framework based on the implementation of both approaches, although time and resources expensive, appears advisable. Stochastic models, then, support the well developed probabilistic model checking analysis. We have extended a model firstly presented in [ 7]. We have incorporated the Cytotoxic T Lymphocytes (CTLs) response and the dynamics of TB opportunistic infection so as to analyse the coinfection of HIV strains and another disease associated with it.
Furthermore, we have introduced an abstract representation of the HAART therapy treatment by altering the model's parameters that rule the dynamics of our model according to the known effects of the treatment. We are presenting results of the analysis of the HIV and the opportunistic TB infection dynamics and an associated therapy through differential equations, stochastic modelling and formal reasoning techniques.
Experiments carried out by means the deterministic model are reported in Figure 2. Details about the construction of the model are reported in the Methods section. For the sake of space we do not show the sensitivity analysis of the deterministic model. Experiments with the model are able to faithfully reproduce well known curves of the virus and CD4 T cells dynamics in absence of TB. The introduction of TB provides a novel description of the dynamics occurring with this infection where viral load increases suddenly in the last stage of HIV1 (AIDS) because of opportunistic diseases (TB) (see [ 33]). In particular, Figure 2(a) shows the behaviour of CD4 T cells during the switch between R5 and X4 strains. The general dynamics of CD4 T cells and viral load can be observed. In the latest stage of HIV1 infection (opportunistic diseases stage) a sudden increase of the viral load can be observed, which lead to AIDS. The increase of TNF against the viral load time course is reported in Figure 2(b). This TNF dynamics provide a clear explanation of the quick growth of viruses when TB infection occurs. TB and X4 strain of HIV stimulate TNF production which, in turn, help them to progress at faster rate.
The model of HIV and TB coinfection can easily be extended to embrace the effect of a common antiHIV treatment such as the HAART. Drug therapies such as HAART and Maraviroc, although with different mechanisms, result in decreasing the number of viruses and the death of infected cells. Exploiting the expressivity of the treatment, we model HAART in terms of its effects. For the sake of simplicity this can be done by changing the virus replication rate ( π, see Methods), reflecting a decreased replication rate and budding from the infected cell. Simulation results are reported in Figure 3. Plots (a) and (b) show the effect of the HAART therapy delivered before and after the appearance of the X4 strain, respectively and before (c) and after (d) the TB infection, respectively. Clearly, both the appearance of X4 and the occurrence of TB infection accelerate the decrease of CD4 T cells which the HAART is able to stop but not to completely reverse. An early start promulgated HAART treatment will change the probability of arising of X4 (this results was obtained by Sguanci et al). Here we show that short HAART treatments have small effect if administrated when CD4 T cells count is above 200 and they have even smaller effect when CD4 T cells counts are below 200.
Many natural and biological phenomena are intrinsically stochastic and discrete, and they can not always be properly described by means of a deterministic and continuous description. For instance, systemic emergent properties can be sensitive to the local presence of minimal (integer) quantities of molecules [ 34]. Roughly speaking, a stochastic model associates a probability to each state transition of the modelled system, expressed as a rate associated to the transition. Associated probability distributions are typically memoryless, and hence the overall system behaviour can be interpreted as a Markov Chain. Often, models are used to simulate possible evolutions of the system from initial conditions, [ 35].
Starting from the deterministic model of HIV, TB and HAART, we have determined a corresponding stochastic model. This has been done via standard transformation from deterministic rates into stochastic ones, according to a fixed reference volume of the model (see, e.g., [ 36]).
Simulation results are reported in Figure 4 about the dynamics observed for a specific possible evolution of the system (chosen according to the probability distribution determined by the model). From Figure 4 (left) it emerges that CD4 T cells, representative of the immune system health, go quickly down in the massive presence of the X4 viral strain. As soon as CD4 T is below a threshold limit, 20 units on the scale of this model, TB develops and the viral load saturates. This reproduces, on a small scale, the general time course at individual level, like the one reported in Figure 2. In Figure 4 (right) a simulation under the same initial conditions is shown. In this case, the HAART treatment has been administered starting at a quite early time point (after few tenth of the initial second) and then stopped (at about 2.5 seconds). It can be observed that, even if HIV progression weakens the immune system, it never goes below the threshold, but rather the viral load seems quite well controlled. In the short interval, HAART prevented the development of TB once started before its insurgence. However the viral load upraises after the interruption of the therapy. The stochastic modeling approach shows important advantages, such as the possibility of pipelining with the probabilistic model checking and some limits in the computational intensive requirement. Work in progress will make use of grid computing facilities (EGEE and Cambridge) and cloud facilities.
Observing the quantitative results of the stochastic simulations in Figure 4, one can have an idea about the fact that the HAART therapy is somehow effective. However, we discuss now an example on how it is possible to move from a correct and informative, but somehow empirical, interpretation of data, as the idea above, to a more precise and formal approach by specifying properties of interest as logical formulae. This has the advantage of requiring a definition of all the aspects of interest, of referring to a formal and unambiguous semantics, and of having an automated procedure for verifying formulae (as the one we adopted [ 20]). Differently, observations rely on the capability of properly interpreting the graphs, which sometimes may appear obscure and difficult to interpret. More details about the methodology can be found in the Methods section.
We focus on two properties that can give a measure of the infection progression.
i) we consider the number of infected cells leading to virus replication as a measure of the spread of infection. We are interested in measuring how often this can occur. This can be expressed by a formula like
where R{" i_to_v"} represents the number of occurrences of an event labelled with i_to_v, i.e. the transition from an infected CD4 T cell to virus replication. The question mark says we are interested in determining the number of such possible occurrences in the model dynamics. C < 5.0 stands for the time interval;
ii) we consider the amount of healthy CD4 T cells, represented by variable tc, as a measure of resistance to the virus attack. We are interested in the probability that tc is less than the threshold 20. Here ? requires the computation of a probability and F [...] tc <= 20 is a logic term expressing that the event tc <= 20 occurs within the interval [...]:
The analysis has been performed using the PRISM model checker (see Methods section). Properties can be validated either by constructing the complete Continuoustime Markov Chain relative to the given model model or by approximating verification through sampling a certain number of possible evolutions. The former can result costly or unfeasible for large models. Adopting the latter we obtained the results reported in Table 1.
HIV+TB  HIV+TB+HAART  

R{" i_to_v"} = ? [ C < = 9.0]  250  269 


P = ? [ F[5.0, 8.0] tc < = 20]  0.885  0.429 
Automated verification yields quantitative measures of the investigated properties. While the number of viral replications due to CD4 T cell infection is comparable (but without HAART many other infected cells contribute to virus replication), the probability of a failure of the immune system is much stronger without HAART treatment, closely to twice as much as.
We have illustrated the potential benefits of formal methods and quantitative models when applied to the study of viral infections and therapy assessment within a computational bioinformatics approach. We have done this by presenting experiments on a proofofconcept scenario regarding HIV infection and the relative TB opportunistic infection. We have adopted an integrated approach, combining deterministic and stochastic techniques and illustrating how properties of interests for the study of viral infections can be formalised in a general purpose logic, as the one supported by PRISM. Our work stresses the growing importance and flexibility of model checking techniques in bioinformatics. Noteworthily, the verification of these properties can precisely characterise the numerical results of simulations, and this can be helpful in comparing and assessing different antiviral therapies. In conclusion, the modelling of HIV infection has two important linked benefits. i) it has matured to the stage of allowing us to combine bioinformatics, computational modelling and formal reasoning techniques, as model checking, i.e. it provides a solid bridge between biological systems and the computational objects used to describe them; ii) these approaches together capture information that can be valuable in therapy validation suggesting the possibility of moving in the future to realistic cases, i.e. translational medicine and clinical bioinformatics.
In this section we provide further details about the construction of the used models and analysis methodologies.
Our work is based on a deterministic model of HIV1 dynamics, firstly appeared in [ 7], which takes into account the models developed by Perelson and his followers [ 3, 10, 13, 37]. These models are well presented and take specific biological reality into account. Our initial model has been extended here by adding two more variables, Cytotoxic T Lymphocytes (CTLs) cells and TB, to capture dynamics of coinfection of HIV and TB.
As standard, we describe the variations of the quantities of the modelled entities as a set of differential equations. We start considering a pool of immature CD4 T cells, represented by the variable U, see equation (1). These cells are continuously produced by the thymus at a rate N _{ U }, and evolve into differentiated, uninfected Tcells, T at a rate δ ^{ U }. Also, the TNF ( F) contributes to the clearance of naive Tcells, via , and naive T cells are produced at fix rate k _{ Z }due to CTLs ( Z) response. T cells ( T) are described by considering their different strains ( T _{ i }), which we do not detail here (see [ 7]). Beyond being produced, they can become infected ( I _{ k }) by interacting with the virus strains V _{ k }at rate β _{ k }, or die at rate δ ^{ T }, (equation (5)). Note that the infection parameter β is not constant over time, but depends on the distribution of the viral strains R5 and X4 [ 9]. Infected T cells are cleared out at a fixed rate, δ ^{ I }, and also due to the action of CTLs with rate , (equation (2)). Equation (6) describes the budding of viruses, i.e. infected cells produce new viruses at rate π, and the fact that virus particles may be nonviable or being cleared out at rate c by immunoglobulin binding and subsequent engulfments by the macrophages. Next equation (3) describes latent TB ( B) in the blood which propagates with the rate α when T cells goes below a given threshold representing the efficacy of the immune system. The equation (7) describes the TNF ( F) dependence on X4 strains and on the presence of TB in the blood and the fact that the efficacy of such a factor naturally decay in time. Finally, the response of Cytotoxic T Lymphocyte cells Z is as in equation (4): CTLs response depends on number of infected cells (I) and is cleared out at fixed rate b. This model is general enough to be used as a framework for fitting real data and simulating superinfection and coinfection patterns.
The stochastic model has been derived from the deterministic one. As a simplification we consider only two viral strains: R5 viral strain ( V5) and X4 viral strain ( V4), and correspondingly only two kinds of infected cells (I4, I5 and I* for the union of the two). Analogously, quasispecies dynamics revert to V5 strains that transform into V4 strains (at rate β _{ k54 }). These two strains are the ones we focus on when observing the time course of infections. As for the deterministic model, we have included sufficient details of interaction among the species to express the properties of interest.
As mentioned, we needed to translate some parameters from deterministic to stochastic ones, accordingly to the reference volume of interest. Other parameters, particularly due to lack of existing data in literature, have been approximated by tuning the model on known macroscopic behaviour. We considered a volume of reaction large enough to contain a statistical reliable number of agents (viruses and cells) and values of extensive quantities are scaled according with the reaction volume considered.
We employ a populationbased approach where the number of each type of species or cells are modelled, rather than the state of each individual component. Furthermore, also according to the PRISM modeling language we used, we rewrote the equations of the deterministic model in terms of a "reactioncentric" description. dynamics is represented by a set of reaction rules stating the involved entities and the results of interaction. These are reported in Table 2. Reaction (02) stands for the production of T cells from naive T cells, while (04) and (05) represent viral infection. Stochastic parameters are on the right part of the Table. Interestingly, parameters α and vary to reflect the emergent behaviour of TB infection against the efficiency of the immune system. when below to a given threshold, the exponential growth of the HIV virus load appears, caused by the spreading of the infection to other cells and abstractly modelled here by such a set of adhoc rules. Initial population of cells in the model is: U = 30, T = 50, I = 30, Z = 30, F = 0, V _{4 }= 50  V _{5}, V _{5 }= 50, B = 10, and the immune deficiency threshold is set to 20.
(01)  N _{ U }= 100  
(02)  δ ^{ U }= 0.1  
(03)  = 0.00001  
(04)  β _{ k5 }= 0.0025  
(05)  β _{ k4 }= 0.0025  
(06)  β _{ k54 }= 0.025  
(07)  δ _{ T }= 0.1  
(08)  δ _{ I }= 0.8  
(09)  δ _{ I }= 0.8  
(10)  k _{ Z }= 0.01  
(11)  = 0.004  
(12)  π = 2.5  
(13)  π = 2.5  
(14)  c _{5 }= 2.5  
(15)  c = 2.5  
(16)  K _{ F }= 0.1  
(17)  α = 2.5 if T <20 otherwise 0  
(18)  K _{ B }= 10  
(19)  = 0.00001 if T < 20 otherwise 0  
(20)  δ ^{ F }= 0.001  
(21)  b = 0.2  
where I* stands for I4 and I5  two rules. 
As far as (the effects of) HAART therapy is concerned, it has been modelled by means of a stochastic triggering event that activates and deactivates the treatment. Activation consists in the modification of interactions (12) and (13), whose rate is downgraded to 1, representing reduced morbidity of the virus, which is one of the main effects of HAART.
Being an introduction to probabilistic model checking beyond the scope of this paper, we refer the interested reader to the cited literature and references therein. Other recent works are [ 15, 16, 38]. We introduce informally the main concepts by examples.
The information encoded in a stochastic model describes, roughly speaking, the states in which the modelled system can find itself and the associated probability of being in a state at a certain time. For many natural phenomena that follow a memoryless probability distribution this amounts to a (Continuous Time) Markov Chain (CTMC). Furthermore, given a stochastic model, several algorithms to simulate the possible quantitative evolutions of the system have been defined, noticeably the Gillespie's algorithm [ 2]. State semantics, such as Transition Systems, have been extensively studied and used to precisely describe the behaviour of dynamical systems, like distributed and concurrent computational systems. State semantics may often become hardly manageable due to the exponential explosion of the number of states. However, several efficient and automated analysis techniques have been defined. Logical formulas can represent "homogeneous" sets of states. A formula like
can be used to represent the set of states in which an " akindof" transition can occur and the system evolves into a state fulfilling, in turn, the formula ϕ. In a sense, the states of the semantics become the model of the formula of interest. The problem of the verification of a formula against a state semantics is known as Model Checking [ 19] and yields either an affirmative answer or a counter example, e.g. a set of states not fulfilling the formula. Most of the times, the model checking procedure is fully automated. Logics [ 39] and model checking procedures [ 40] have been defined for probabilistic state semantics, that is Probabilistic Model Checking. A typical logic may express formulas like
which, informally speaking, represents all the traces for which ϕ holds with probability bigger than p. Other examples are F >= t x > 2, the traces in which eventually x > 2 after t time units, and G x < 10, globally, for all the traces, the value of x is less than 10.
The PRISM probabilistic model checker [ 20] is a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. Beyond CTMC, PRISM also supports DTCM and Markov decision processes [ 41]. PRISM has been chosen as it is one of the reference existing model checker, free and open source. However, its features are not determinant here, and other similar platforms could have been chosen. PRISM models are specified in a formal language that describes the entities present in the model, their behaviour and their quantities. One or more entities can participate synchronously to an event that causes a state change. The state typically consists of the values of the variables of the model. As seen, T cell infection is an event to which virus strains and T cell participate. This event leads to an increased number of infected cells, and less T cells and viruses, which have been combined together. Participation to events has stochastic rates associated. The quantities of entities affect the stochastic dynamics as expected. Figure 5 shows the code for T cell. The variable tc keeps trace of the amount of T cells, then two of the possible interactions for T cells are reported, each consisting of a name, an integrity constraint, a rate and an effect: [ o2] generation of a new T cell, and [ o5] infection. The [ o5] interaction is shared with Virus X4 and I cell (see Table 2). As a consequence of the occurrence of such interaction, the former decreases its amount v4' = v4 1, which is required to be nonnegative, while the amount of the latter is instead increased. It is worth noting how rates are defined so as to respect stochastic semantics. Rates of synchronously executed actions are multiplied to determine the overall rate of the corresponding transition, i.e. the parameter of the negative exponential distribution associated. In the case of [ o5], the overall rate is correctly determined by multiplying the amount of T cell and Virus X4 together with the rate B _{ k4 }. A PRISM model can be used for simulation purposes, and for exact or approximated model checking as illustrated.
The authors declare that they have no competing interests.
AS and PL authors have studied the deterministic model of infection used in this paper. PL author has investigated the phylogenetic information. AS and AB authors have defined the stochastic version of the model and run insilico experiments. All authors have worked on experiments results.
The authors wish to thank the anonymous referees for their helpful comments on a previous version of this paper. This project is partially supported by EC IST SOCIALNETS and WADA projects.
This article has been published as part of BMC Bioinformatics Volume 11 Supplement 1, 2010: Selected articles from the Eighth AsiaPacific Bioinformatics Conference (APBC 2010). The full contents of the supplement are available online at http://www.biomedcentral.com/14712105/11?issue=S1.
1 
Lió P, Vannucci MFinding pathogenicity islands and gene transfer events in genome dataBioinformatics(2000) 16: 932940 10.1093/bioinformatics/16.10.932 Pubmed ID: 11120683 
2 
Gillespie DTExact Stochastic Simulation of Coupled Chemical ReactionsThe Journal of Physical Chemistry(1977) 81: 2523402361 10.1021/j100540a008 
3 
Ho D, Neumann AU, Perelson AS, Chen W, Leonard JM, M MRapid turnover of plasma virions and CD4 lymphocytes in HIV1 infectionNature(1995) 373: 123126 10.1038/373123a0 Pubmed ID: 7816094 
4 
Nowak MA, May RMVirus dynamics. mathematical principles of immunology and virology(2000) Oxford University Press 
5 
Perelson ASModelling viral and immune system dynamicsNature Review Immunology(2002) 2: 12836 10.1038/nri700 
6 
Eigen M, McCaskill J, Schuster PThe Molecular QuasiSpeciesAdvances in Chemical Physics(1989) 75: 149263full_text 
7 
Sguanci L, Bagnoli F, Li PModeling HIV quasispecies evolutionary dynamicsBMC Evolutionary Biology(2007) 7: 2S5 10.1186/147121487S2S5 Pubmed ID: 17767733 
8 
Ronga L, Perelson ASModeling HIV persistence, the latent reservoir, and viral blipsJournal of Theoretical Biology(2009) 
9 
Bagnoli F, Lio' P, Sguanci LModeling viral coevolution. HIV multiclonal persistence and competition dynamicsPhysica A(2005) 366: 333346 10.1016/j.physa.2005.10.055 
10 
Chao L, Davenport MP, Forrest S, Perelson ASA stochastic model of cytotoxic T cell responsesJournal Theoretical Biology(2004) 228: 227240 10.1016/j.jtbi.2003.12.011 
11 
Celada F, Seiden PEAffinity maturation and hypermutation in a simulation of the humoral immune responseJournal of Theoretical Biology(1996) 26: 13501358 
12 
De Boer RJ, Perelson ASTowards a general function describing T cell proliferationEuropean Journal of Immunology(1995) 175: 4567576 
13 
Wiegel FW, Perelson ASSome scaling principles for the immune systemImmunology and Cell Biology(2004) 82: 127131 10.1046/j.08189641.2004.01229.x Pubmed ID: 15061763 
14 
Regev A, Shapiro ECells as computationNature(2002) 419: 343 10.1038/419343a Pubmed ID: 12353013 
15 
Mateus D, Gallois JP, Comet eaSymbolic modeling of genetic regulatory networksJournal of Bioinformatics and Computational Biology(2007) 5: 2B627640 10.1142/S0219720007002850 Pubmed ID: 17636866 
16 
Fromentin J, Comet JP, Le Gall P, Roux OAnalysing gene regulatory networks by both constraint programming and modelcheckingConference proceedings, IEEE Engineering in Medicine and Biology(2007) 45954598 
17 
Batt G, Yordanov B, Weiss R, Belta CRobustness analysis and tuning of synthetic gene networksBioinformatics(2007) 23: 24152422 10.1093/bioinformatics/btm362 Pubmed ID: 17660209 
18 
Batt G, Ropers D, De Jong H, Geiselmann J, Mateescu R, Page M, Schneider DValidation of qualitative models of genetic regulatory networks by model checking. Analysis of the nutritional stress response in E. coliBioinformatics(2005) 21: Suppl 1i19i28 10.1093/bioinformatics/bti1048 Pubmed ID: 15961457 
19 
Clarke EM, Grumberg O, Peled DAModel Checking(1999) The MIT Press 
20 
The PRISM model checker http://www.prismmodelchecker.org 
21 
Karlsson I, Antonsson L, Shi Y, Oberg M, Karlsson A, Albert J, Olde B, Owman C, M J, Fenyo EMCoevolution of RANTES sensitivity and mode of CCR5 receptor use by human immunodeficiency virus type 1 of the R5 phenotypeJournal of Virology(2004) 78: 1180711815 10.1128/JVI.78.21.1180711815.2004 Pubmed ID: 15479822 
22 
Gorry PR, Churchill M, Crowe SM, Cunningham AL, Gabuzda DPathogenesis of macrophage tropic HIVCurrent HIV Research(2005) 3: 5360 10.2174/1570162052772951 Pubmed ID: 15638723 
23 
Gray L, Sterjovski J, Churchill M, Ellery P, Nasr N, Lewin SR, Crowe SM, Wesselingh SL, Cunningham AL, Gorry PRUncoupling coreceptor usage of human immunodeficiency virus type 1 (HIV1) from macrophage tropism reveals biological properties of CCR5restricted HIV1 isolates from patients with acquired immunodeficiency syndromeVirology(2005) 337: 384398 10.1016/j.virol.2005.04.034 Pubmed ID: 15916792 
24 
Pavlakis GN, Valentin A, Morrow M, Yarchoan RDifferential effects of TNF on HIV1 expression. R5 inhibition and implications for viral evolutionInternation Conference AIDS(2004) 15: 1116 
25 
Parczewski M, LeszczyszynPynka M, M K, Adler G, BinczakKuleta A, Loniewska B, BoronKaczmarska A, Ciechanowicz ASequence variants of chemokine receptor genes and susceptibility to HIV1 infectionJournal of Applied Genetics(2009) 50: 2159166 Pubmed ID: 19433914 
26 
Hatse S, Huskens D, Princen K, Vermeire K, Bridger GJ, De Clercq E, Rosenkilde MM, Schwartz TW, D SModest human immunodeficiency virus coreceptor function of CXCR3 is strongly enhanced by mimicking the CXCR4 ligand binding pocket in the CXCR3 receptorJournal of Virology(2007) 81: 736323639 10.1128/JVI.0194106 Pubmed ID: 17251291 
27 
Wen W, Chen S, Cao Y, Zhu Y, Yamamoto YHIV1 infection initiates changes in the expression of a wide array of genes in U937 promonocytes and HUT78 T cellsVirus Research(2005) 113: 12635 10.1016/j.virusres.2005.04.002 Pubmed ID: 15885842 
28 
MayanjaKizza H, Wu M, Aung H, Liu S, Luzze H, Hirsch C, Z TThe interaction of monocyte chemoattractant protein1 and tumour necrosis factoralpha in Mycobacterium tuberculosisinduced HIV1 replication at sites of active tuberculosisScandinavian Journal of Immunology(2009) 69: 6516520 10.1111/j.13653083.2009.02246.x Pubmed ID: 19439012 
29 
Maddocks S, Scandurra GM, Nourse C, Bye C, Williams RB, Slobedman B, Cunningham AL, J BWGene expression in HIV1/Mycobacterium tuberculosis coinfected macrophages is dominated by M. tuberculosisTuberculosis (Edinb)(2009) 89: 4285293 10.1016/j.tube.2009.05.003 Pubmed ID: 19520608 
30 
Volpe E, Cappelli G, Grassi M, Martino A, Serafino A, Colizzi V, Sanarico N, Mariani FGene expression profiling of human macrophages at late time of infection with Mycobacterium tuberculosisImmunology(2006) 118: 4449460 Pubmed ID: 16895554 
31 
Hirano F, Komura K, Fukawa E, Makino ITumor necrosis factor alpha (TNFalpha)induced RANTES chemokine expression via activation of NFkappaB and p38 MAP kinase. roles of TNFalpha in alcoholic liver diseasesJournal of Hepatology(2003) 38: 4483489 10.1016/S01688278(02)004567 Pubmed ID: 12663241 
32 
Ranjbar S, Boshoff HI, Mulder A, Siddiqi N, Rubin EJ, Goldfeld AEHIV1 replication is differentially regulated by distinct clinical strains of Mycobacterium tuberculosisPLoS One(2009) 4: 7e6116 10.1371/journal.pone.0006116 Pubmed ID: 19568431 
33 
Collins KR, QuinonesMateu ME, Wu M, Luzze H, Johnson JL, Hirsch C, Toossi Z, Arts EJHuman immunodeficiency virus type 1 (HIV1) quasispecies at the sites of Mycobacterium tuberculosis infection contribute to systemic HIV1 heterogeneityJournal of Virology(2002) 76: 416971706 10.1128/JVI.76.4.16971706.2002 Pubmed ID: 11799165 
34 
Wilkinson DStochastic Modelling for Systems Biology(2006) CRC press 
35 
VanKampen NGStochastic processes in physics and in chemistry(1992) Elsevier, Amsterdam 
36 
Kierzek AMStocks. Stochastic kinetic simulations of biochemical system with Gillespie algorithmBioinformatics(2002) 18: 470481 10.1093/bioinformatics/18.3.470 Pubmed ID: 11934747 
37 
Perelson AS, Neumann AU, Markowitz M, Leonard JM, Ho DDHIV1 Dynamics in Vivo. Virion Clearance Rate, Infected Cell LifeSpan, and Viral Generation TimeScience(1996) 271: 15821586 10.1126/science.271.5255.1582 Pubmed ID: 8599114 
38 
Fisher J, Piterman N, Hajnal A, Henzinger TAPredictive modeling of signaling crosstalk during C. elegans vulval developmentPLoS Computational Biology(2007) 3: 5e92 10.1371/journal.pcbi.0030092 Pubmed ID: 17511512 
39 
Aziz A, Sanwal K, Singhal V, Brayton RModel checking continuous time Markov chainsACM Transactions on Computational Logic(2000) 1: 1162170 10.1145/343369.343402 
40 
Baier C, Haverkort B, Hermanns H, Katoen JPModelchecking algorithms for continuoustime Markov chainsIEEE Transactions on Software Engineering(2003) 29: 6524541 10.1109/TSE.2003.1205180 
41 
Kwiatkowska M, Norman G, Parker DCondon A, Harel D, Kok J, Salomaa A, Winfree EQuantitative Verification Techniques for Biological Processes(2009) Algorithmic Bioprocesses, Springer 
42 
Bruch CL, Chao LEvolvability of an RNA virus determined by its mutational neighborhoodNature(2000) 406: 625628 10.1038/35020564 Pubmed ID: 10949302 
43 
Asquith B, Edwards CTT, Lipsitch M, McLean ARInefficient Cytotoxic T Lymphocyte Mediated Killing of HIV1 Infected Cells In VivoPLOS Biology(2006) 4: 4e90 10.1371/journal.pbio.0040090 Pubmed ID: 16515366 
44 
Althaus CL, Be Boer RJDynamics of Immune escape during HIV/SIV InfectionPLOS Computational Biology(2008) 4: 7e1000103 10.1371/journal.pcbi.1000103 Pubmed ID: 18636096 