A Model Checking Approach to Discrete Bifurcation Analysis
| Authors | |
|---|---|
| Year of publication | 2016 |
| Type | Article in Proceedings |
| Conference | Formal Methods. FM 2016 |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-319-48989-6_6 |
| Field | Informatics |
| Keywords | model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms; bifurcation analysis |
| Description | Bifurcation analysis is a central task of the analysis of parameterised high-dimensional dynamical systems that undergo transitions as parameters are changed. The classical numerical and analytical methods are typically limited to a small number of system parameters. In this paper we propose a novel approach to bifurcation analysis that is based on a suitable discrete abstraction of the 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. We demonstrate the method on a case study taken from systems biology. |
| Related projects: |