Cargando…

Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors

At the crossroad between biology and mathematical modeling, computational systems biology can contribute to a mechanistic understanding of high-level biological phenomenon. But as knowledge accumulates, the size and complexity of mathematical models increase, calling for the development of efficient...

Descripción completa

Detalles Bibliográficos
Autores principales: Hernandez, Céline, Thomas-Chollier, Morgane, Naldi, Aurélien, Thieffry, Denis
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Frontiers Media S.A. 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7554341/
https://www.ncbi.nlm.nih.gov/pubmed/33101049
http://dx.doi.org/10.3389/fphys.2020.558606
_version_ 1783593754688487424
author Hernandez, Céline
Thomas-Chollier, Morgane
Naldi, Aurélien
Thieffry, Denis
author_facet Hernandez, Céline
Thomas-Chollier, Morgane
Naldi, Aurélien
Thieffry, Denis
author_sort Hernandez, Céline
collection PubMed
description At the crossroad between biology and mathematical modeling, computational systems biology can contribute to a mechanistic understanding of high-level biological phenomenon. But as knowledge accumulates, the size and complexity of mathematical models increase, calling for the development of efficient dynamical analysis methods. Here, we propose the use of two approaches for the development and analysis of complex cellular network models. A first approach, called "model verification" and inspired by unitary testing in software development, enables the formalization and automated verification of validation criteria for whole models or selected sub-parts. When combined with efficient analysis methods, this approach is suitable for continuous testing, thereby greatly facilitating model development. A second approach, called "value propagation," enables efficient analytical computation of the impact of specific environmental or genetic conditions on the dynamical behavior of some models. We apply these two approaches to the delineation and the analysis of a comprehensive model for T cell activation, taking into account CTLA4 and PD-1 checkpoint inhibitory pathways. While model verification greatly eases the delineation of logical rules complying with a set of dynamical specifications, propagation provides interesting insights into the different potential of CTLA4 and PD-1 immunotherapies. Both methods are implemented and made available in the all-inclusive CoLoMoTo Docker image, while the different steps of the model analysis are fully reported in two companion interactive jupyter notebooks, thereby ensuring the reproduction of our results.
format Online
Article
Text
id pubmed-7554341
institution National Center for Biotechnology Information
language English
publishDate 2020
publisher Frontiers Media S.A.
record_format MEDLINE/PubMed
spelling pubmed-75543412020-10-22 Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors Hernandez, Céline Thomas-Chollier, Morgane Naldi, Aurélien Thieffry, Denis Front Physiol Physiology At the crossroad between biology and mathematical modeling, computational systems biology can contribute to a mechanistic understanding of high-level biological phenomenon. But as knowledge accumulates, the size and complexity of mathematical models increase, calling for the development of efficient dynamical analysis methods. Here, we propose the use of two approaches for the development and analysis of complex cellular network models. A first approach, called "model verification" and inspired by unitary testing in software development, enables the formalization and automated verification of validation criteria for whole models or selected sub-parts. When combined with efficient analysis methods, this approach is suitable for continuous testing, thereby greatly facilitating model development. A second approach, called "value propagation," enables efficient analytical computation of the impact of specific environmental or genetic conditions on the dynamical behavior of some models. We apply these two approaches to the delineation and the analysis of a comprehensive model for T cell activation, taking into account CTLA4 and PD-1 checkpoint inhibitory pathways. While model verification greatly eases the delineation of logical rules complying with a set of dynamical specifications, propagation provides interesting insights into the different potential of CTLA4 and PD-1 immunotherapies. Both methods are implemented and made available in the all-inclusive CoLoMoTo Docker image, while the different steps of the model analysis are fully reported in two companion interactive jupyter notebooks, thereby ensuring the reproduction of our results. Frontiers Media S.A. 2020-09-30 /pmc/articles/PMC7554341/ /pubmed/33101049 http://dx.doi.org/10.3389/fphys.2020.558606 Text en Copyright © 2020 Hernandez, Thomas-Chollier, Naldi and Thieffry. http://creativecommons.org/licenses/by/4.0/ This is an open-access article distributed under the terms of the Creative Commons Attribution License (CC BY). The use, distribution or reproduction in other forums is permitted, provided the original author(s) and the copyright owner(s) are credited and that the original publication in this journal is cited, in accordance with accepted academic practice. No use, distribution or reproduction is permitted which does not comply with these terms.
spellingShingle Physiology
Hernandez, Céline
Thomas-Chollier, Morgane
Naldi, Aurélien
Thieffry, Denis
Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title_full Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title_fullStr Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title_full_unstemmed Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title_short Computational Verification of Large Logical Models—Application to the Prediction of T Cell Response to Checkpoint Inhibitors
title_sort computational verification of large logical models—application to the prediction of t cell response to checkpoint inhibitors
topic Physiology
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7554341/
https://www.ncbi.nlm.nih.gov/pubmed/33101049
http://dx.doi.org/10.3389/fphys.2020.558606
work_keys_str_mv AT hernandezceline computationalverificationoflargelogicalmodelsapplicationtothepredictionoftcellresponsetocheckpointinhibitors
AT thomascholliermorgane computationalverificationoflargelogicalmodelsapplicationtothepredictionoftcellresponsetocheckpointinhibitors
AT naldiaurelien computationalverificationoflargelogicalmodelsapplicationtothepredictionoftcellresponsetocheckpointinhibitors
AT thieffrydenis computationalverificationoflargelogicalmodelsapplicationtothepredictionoftcellresponsetocheckpointinhibitors