A Model Checking Approach to Discrete Bifurcation Analysis

N. Beneš, L. Brim, M. Demko, S. Pastva, D. Šafránek

Formal Methods (FM) 2016

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.

Cite this paper as: Beneš N., Brim L., Demko M., Pastva S., Šafránek D. (2016) A Model Checking Approach to Discrete Bifurcation Analysis. In: Fitzgerald J., Heitmeyer C., Gnesi S., Philippou A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science, vol 9995. Springer, Cham