Model Checking Approach to Discrete Bifurcation Analysis

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BENEŠ Nikola BRIM Luboš DEMKO Martin ŠAFRÁNEK David PASTVA Samuel HAJNAL Matej

Year of publication 2017
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Description Continuous dynamical systems can be used to study a wide variety of phenomena in biology, economy, engineering and computer science. These systems usually contain parameters which significantly influence their behaviour. Such influence is traditionally studied using the apparatus of bifurcation analysis. However, current numerical and analytical methods for bifurcation analysis are hard to automatise, do not scale well in the number of parameters, and are often limited to specific canonical models. In this work, we present a novel approach to bifurcation analysis which assumes a suitable discrete abstraction of the continuous system and employs model checking to discover the critical parameter values, referred to as bifurcation points. To distinguish a qualitative change in the system's behaviour, we rely on the notion of behavioural patterns (cycle, equilibrium, saddle, etc.), also known as phase portraits. We define a hybrid extension of CTL logic with direction formulae in order to specify such patterns. We demonstrate the method on a model of a bistable genetic switch mechanism taken from systems biology.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info