Discrete Bifurcation Analysis with Pithya

D 2017

Discrete Bifurcation Analysis with Pithya

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

Basic information

Original name

Discrete Bifurcation Analysis with Pithya

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Martin DEMKO (703 Slovakia, belonging to the institution), Matej HAJNAL (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/17:00114985

Organization unit

Faculty of Informatics

ISBN

978-3-319-67470-4

ISSN

UT WoS

000542715600021

Keywords in English

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

Abstract

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.

Links

GA15-11089S, research and development project

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

Investor: Czech Science Foundation

LM2015055, research and development project

Name: Centrum pro systémovou biologii (Acronym: C4SYS)

Investor: Ministry of Education, Youth and Sports of the CR

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Matej HAJNAL, Samuel PASTVA and 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, p. 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 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.

Detailed Information on Publication Record