Discrete Bifurcation Analysis with Pithya

D 2017

Discrete Bifurcation Analysis with Pithya

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Matej HAJNAL, Samuel PASTVA et. al.

Základní údaje

Originální název

Discrete Bifurcation Analysis with Pithya

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Martin DEMKO (703 Slovensko, domácí), Matej HAJNAL (703 Slovensko, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, garant, domácí)

Vydání

LNCS 10545. Cham, 15th International Conference on Computational Methods in Systems Biology (CMSB), od s. 319-320, 2 s. 2017

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/17:00114985

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-67470-4

ISSN

UT WoS

000542715600021

Klíčová slova anglicky

bifurcation analysis; model checking; systems biology; terminal strongly connected components; parameter synthesis; parallel algorithms

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2021 17:30, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA15-11089S, projekt VaV

Název: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů

LM2015055, projekt VaV

Název: Centrum pro systémovou biologii (Akronym: C4SYS)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, The national infrastructure C4SYS - Centre for Systems Biology

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Matej HAJNAL, Samuel PASTVA a David ŠAFRÁNEK. Discrete Bifurcation Analysis with Pithya. In Feret J. et al. 15th International Conference on Computational Methods in Systems Biology (CMSB). LNCS 10545. Cham: Springer, 2017, s. 319-320. ISBN 978-3-319-67470-4.

@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 a 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, s.~319-320. ISBN~978-3-319-67470-4.

Podrobný výpis o publikaci