Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1394275,
author = {Beneš, Nikola and Brim, Luboš and Demko, Martin and Hajnal, Matej and Pastva, Samuel and Šafránek, David},
address = {Cham},
booktitle = {15th International Conference on Computational Methods in Systems Biology (CMSB)},
edition = {LNCS 10545},
editor = {Feret J. et al.},
keywords = {bifurcation analysis; model checking; systems biology; terminal strongly connected components; parameter synthesis; parallel algorithms},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Cham},
isbn = {978-3-319-67470-4},
pages = {319-320},
publisher = {Springer},
title = {Discrete Bifurcation Analysis with Pithya},
year = {2017}
}
TY - JOUR
ID - 1394275
AU - Beneš, Nikola - Brim, Luboš - Demko, Martin - Hajnal, Matej - Pastva, Samuel - Šafránek, David
PY - 2017
TI - Discrete Bifurcation Analysis with Pithya
PB - Springer
CY - Cham
SN - 9783319674704
KW - bifurcation analysis
KW - model checking
KW - systems biology
KW - terminal strongly connected components
KW - parameter synthesis
KW - parallel algorithms
N2 - Bifurcation analysis is a central task of the analysis of parameterised high-dimensional dynamical systems that undergo transitions as parameters are changed. To characterise such transitions for models with many unknown parameters is a major challenge for complex, hence more realistic, models in systems biology. Its difficulty rises exponentially with the number of model components. The classical numerical and analytical methods for bifurcation analysis are typically limited to a small number of independent system parameters. To address this limitation we have developed a novel approach to bifurcation analysis called discrete bifurcation analysis, that is based on a suitable discrete abstraction of the given system and employs model checking for discovering critical parameter values, referred to as bifurcation points, for which various kinds of behaviour (equilibrium, cycling) appear or disappear. To describe such behaviour patterns, called phase portraits, we use a hybrid version of a CTL logic augmented with direction formulae. Technically, our approach is grounded in a novel method of parameter synthesis from temporal logic formulae using symbolic model checking and implemented in a new high-performance tool Pithya. Pithya itself implements state-of-the-art parameter synthesis methods. For a given ODE model, it allows to visually explore model behaviour with respect to different parameter values. Moreover, Pithya automatically synthesises parameter values satisfying a given property. Such property can specify various behaviour constraints, e.g., maximal reachable concentration, time ordering of events, characteristics of steady states, the presence of limit cycles, etc. The results can be visualised and explored in a graphical user interface. We demonstrate the method on a case study taken from biology describing the interaction of the tumour suppressor protein pRB and the central transcription factor E2F1. This system represents an important mechanism of a biological switch governing the transition from G1 to S phase in the mammalian cell cycle. In the G1-phase the cell makes an important decision. In high concentration levels, E2F1 activates the phase transition. In low concentration of E2F1, the transition to S-phase is rejected and the cell avoids division.
ER -
BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Matej HAJNAL, Samuel PASTVA and David ŠAFRÁNEK. Discrete Bifurcation Analysis with Pithya. In Feret J. et al. \textit{15th International Conference on Computational Methods in Systems Biology (CMSB)}. LNCS 10545. Cham: Springer, 2017, p.~319-320. ISBN~978-3-319-67470-4.
|
