Discrete Bifurcation Analysis with Pithya
| Authors | |
|---|---|
| Year of publication | 2017 |
| Type | Article in Proceedings |
| Conference | 15th International Conference on Computational Methods in Systems Biology (CMSB) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | bifurcation analysis; model checking; systems biology; terminal strongly connected components; parameter synthesis; parallel algorithms |
| 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. |
| Related projects: |