Limits...
Model checking to assess T-helper cell plasticity.

Abou-Jaoudé W, Monteiro PT, Naldi A, Grandclaudon M, Soumelis V, Chaouiya C, Thieffry D - Front Bioeng Biotechnol (2015)

Bottom Line: To account for novel cellular subtypes, we present an extended version of a published model of Th cell differentiation.We then use symbolic model checking to analyze reachability properties between Th subtypes upon changes of environmental cues.Finally, we explore novel strategies enabling specific Th cell polarizing or reprograming events.

View Article: PubMed Central - PubMed

Affiliation: Institut de Biologie de l'Ecole Normale Supérieure , Paris , France ; UMR CNRS 8197 , Paris , France ; INSERM U1024 , Paris , France ; Laboratoire d'Informatique de l'Ecole Normale Supérieure , Paris , France.

ABSTRACT
Computational modeling constitutes a crucial step toward the functional understanding of complex cellular networks. In particular, logical modeling has proven suitable for the dynamical analysis of large signaling and transcriptional regulatory networks. In this context, signaling input components are generally meant to convey external stimuli, or environmental cues. In response to such external signals, cells acquire specific gene expression patterns modeled in terms of attractors (e.g., stable states). The capacity for cells to alter or reprogram their differentiated states upon changes in environmental conditions is referred to as cell plasticity. In this article, we present a multivalued logical framework along with computational methods recently developed to efficiently analyze large models. We mainly focus on a symbolic model checking approach to investigate switches between attractors subsequent to changes of input conditions. As a case study, we consider the cellular network regulating the differentiation of T-helper (Th) cells, which orchestrate many physiological and pathological immune responses. To account for novel cellular subtypes, we present an extended version of a published model of Th cell differentiation. We then use symbolic model checking to analyze reachability properties between Th subtypes upon changes of environmental cues. This allows for the construction of a synthetic view of Th cell plasticity in terms of a graph connecting subtypes with arcs labeled by input conditions. Finally, we explore novel strategies enabling specific Th cell polarizing or reprograming events.

No MeSH data available.


Related in: MedlinePlus

Reprograming graph, considering all canonical Th subtypes, generated with the model checker NuSMV-ARCTL. Nodes represent sets of states characterizing the canonical Th subtypes defined in Table 2. There is an arc labeled with e, going from node c1 to node c2, whenever the following ARCTL temporal logic formula is verified: INIT c1; EAF (e) (c2 ∧ AAG (e)(c2)). It should be noted that the existence of a single reprograming path from a Th subtype to another one does not necessarily imply the stability of the target Th subtype, since NuSMV-ARCTL considers that a property is true if and only if it is verified by the whole set of states in the initial conditions. Hence, if at least one state associated with a given subtype points to a state not associated with this subtype (for given input conditions), then the stability of the Th subtype is not represented (see for example, Th9 subtype, which is not considered stable under proTh9 input condition).
© Copyright Policy - open-access
Related In: Results  -  Collection

License
getmorefigures.php?uid=PMC4309205&req=5

Figure 3: Reprograming graph, considering all canonical Th subtypes, generated with the model checker NuSMV-ARCTL. Nodes represent sets of states characterizing the canonical Th subtypes defined in Table 2. There is an arc labeled with e, going from node c1 to node c2, whenever the following ARCTL temporal logic formula is verified: INIT c1; EAF (e) (c2 ∧ AAG (e)(c2)). It should be noted that the existence of a single reprograming path from a Th subtype to another one does not necessarily imply the stability of the target Th subtype, since NuSMV-ARCTL considers that a property is true if and only if it is verified by the whole set of states in the initial conditions. Hence, if at least one state associated with a given subtype points to a state not associated with this subtype (for given input conditions), then the stability of the Th subtype is not represented (see for example, Th9 subtype, which is not considered stable under proTh9 input condition).

Mentions: Checking this property for all the combinations of canonical Th patterns and input conditions, one can represent the verified properties through a reprograming graph, which here abstracts paths between Th patterns and recapitulates the polarizing and reprograming events predicted by our model (Figure 3). This graph provides a global and synthetic representation of Th plasticity depending on environmental cues. Focusing on polarizing events from naive Th0 cells to the other Th subtypes, our model is consistent with experimental data, showing that each canonical subtype can be reached from the naive state Th0 (blue arcs starting from Th0 in Figure 3) in the presence of specific polarizing cytokine combinations (denoted by the labels associated with the blue arcs in Figure 3). The remaining Th subtype conversions present in the reprograming graph would need to be assessed experimentally.


Model checking to assess T-helper cell plasticity.

Abou-Jaoudé W, Monteiro PT, Naldi A, Grandclaudon M, Soumelis V, Chaouiya C, Thieffry D - Front Bioeng Biotechnol (2015)

Reprograming graph, considering all canonical Th subtypes, generated with the model checker NuSMV-ARCTL. Nodes represent sets of states characterizing the canonical Th subtypes defined in Table 2. There is an arc labeled with e, going from node c1 to node c2, whenever the following ARCTL temporal logic formula is verified: INIT c1; EAF (e) (c2 ∧ AAG (e)(c2)). It should be noted that the existence of a single reprograming path from a Th subtype to another one does not necessarily imply the stability of the target Th subtype, since NuSMV-ARCTL considers that a property is true if and only if it is verified by the whole set of states in the initial conditions. Hence, if at least one state associated with a given subtype points to a state not associated with this subtype (for given input conditions), then the stability of the Th subtype is not represented (see for example, Th9 subtype, which is not considered stable under proTh9 input condition).
© Copyright Policy - open-access
Related In: Results  -  Collection

License
Show All Figures
getmorefigures.php?uid=PMC4309205&req=5

Figure 3: Reprograming graph, considering all canonical Th subtypes, generated with the model checker NuSMV-ARCTL. Nodes represent sets of states characterizing the canonical Th subtypes defined in Table 2. There is an arc labeled with e, going from node c1 to node c2, whenever the following ARCTL temporal logic formula is verified: INIT c1; EAF (e) (c2 ∧ AAG (e)(c2)). It should be noted that the existence of a single reprograming path from a Th subtype to another one does not necessarily imply the stability of the target Th subtype, since NuSMV-ARCTL considers that a property is true if and only if it is verified by the whole set of states in the initial conditions. Hence, if at least one state associated with a given subtype points to a state not associated with this subtype (for given input conditions), then the stability of the Th subtype is not represented (see for example, Th9 subtype, which is not considered stable under proTh9 input condition).
Mentions: Checking this property for all the combinations of canonical Th patterns and input conditions, one can represent the verified properties through a reprograming graph, which here abstracts paths between Th patterns and recapitulates the polarizing and reprograming events predicted by our model (Figure 3). This graph provides a global and synthetic representation of Th plasticity depending on environmental cues. Focusing on polarizing events from naive Th0 cells to the other Th subtypes, our model is consistent with experimental data, showing that each canonical subtype can be reached from the naive state Th0 (blue arcs starting from Th0 in Figure 3) in the presence of specific polarizing cytokine combinations (denoted by the labels associated with the blue arcs in Figure 3). The remaining Th subtype conversions present in the reprograming graph would need to be assessed experimentally.

Bottom Line: To account for novel cellular subtypes, we present an extended version of a published model of Th cell differentiation.We then use symbolic model checking to analyze reachability properties between Th subtypes upon changes of environmental cues.Finally, we explore novel strategies enabling specific Th cell polarizing or reprograming events.

View Article: PubMed Central - PubMed

Affiliation: Institut de Biologie de l'Ecole Normale Supérieure , Paris , France ; UMR CNRS 8197 , Paris , France ; INSERM U1024 , Paris , France ; Laboratoire d'Informatique de l'Ecole Normale Supérieure , Paris , France.

ABSTRACT
Computational modeling constitutes a crucial step toward the functional understanding of complex cellular networks. In particular, logical modeling has proven suitable for the dynamical analysis of large signaling and transcriptional regulatory networks. In this context, signaling input components are generally meant to convey external stimuli, or environmental cues. In response to such external signals, cells acquire specific gene expression patterns modeled in terms of attractors (e.g., stable states). The capacity for cells to alter or reprogram their differentiated states upon changes in environmental conditions is referred to as cell plasticity. In this article, we present a multivalued logical framework along with computational methods recently developed to efficiently analyze large models. We mainly focus on a symbolic model checking approach to investigate switches between attractors subsequent to changes of input conditions. As a case study, we consider the cellular network regulating the differentiation of T-helper (Th) cells, which orchestrate many physiological and pathological immune responses. To account for novel cellular subtypes, we present an extended version of a published model of Th cell differentiation. We then use symbolic model checking to analyze reachability properties between Th subtypes upon changes of environmental cues. This allows for the construction of a synthetic view of Th cell plasticity in terms of a graph connecting subtypes with arcs labeled by input conditions. Finally, we explore novel strategies enabling specific Th cell polarizing or reprograming events.

No MeSH data available.


Related in: MedlinePlus