Discrete Bifurcation Analysis with Pithya

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F17%3A00114985" target="_blank" >RIV/00216224:14330/17:00114985 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Discrete Bifurcation Analysis with Pithya

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2017

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

15th International Conference on Computational Methods in Systems Biology (CMSB)

ISBN

9783319674704

ISSN

0302-9743

e-ISSN

—

Number of pages

2

Pages from-to

319-320

Publisher name

Springer

Place of publication

Cham

Event location

Darmstadt

Event date

Sep 27, 2017

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000542715600021