Model Checking Approach to Discrete Bifurcation Analysis

k 2017

Model Checking Approach to Discrete Bifurcation Analysis

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA et. al.

Basic information

Original name

Model Checking Approach to Discrete Bifurcation Analysis

Authors

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

Edition

Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2017

Other information

Language

English

Type of outcome

Prezentace na konferencích

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

URL

Organization unit

Faculty of Informatics

Keywords in English

model checking, bifurcation analysis, parameters, phase portrait, temporal logic

Abstract

V originále

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.

Links

GA15-11089S, research and development project

Name: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Czech Science Foundation

LM2015055, research and development project

Name: Centrum pro systémovou biologii (Acronym: C4SYS)

Investor: Ministry of Education, Youth and Sports of the CR

MUNI/A/0945/2015, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

Investor: Masaryk University, Category A

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA and Matej HAJNAL. Model Checking Approach to Discrete Bifurcation Analysis. In Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2017.

@proceedings{1392805,
   author = {Beneš, Nikola and Brim, Luboš and Demko, Martin and Šafránek, David and Pastva, Samuel and Hajnal, Matej},
   booktitle = {Doctoral Workshop on Mathematical and Engineering Methods in Computer Science},
   keywords = {model checking, bifurcation analysis, parameters, phase portrait, temporal logic},
   language = {eng},
   title = {Model Checking Approach to Discrete Bifurcation Analysis},
   url = {http://www.memics.cz/2017/},
   year = {2017}
}

TY  - CONF
ID  - 1392805
AU  - Beneš, Nikola - Brim, Luboš - Demko, Martin - Šafránek, David - Pastva, Samuel - Hajnal, Matej
PY  - 2017
TI  - Model Checking Approach to Discrete Bifurcation Analysis
KW  - model checking, bifurcation analysis, parameters, phase portrait, temporal logic
UR  - http://www.memics.cz/2017/
N2  - 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.
ER  -

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA and Matej HAJNAL. Model Checking Approach to Discrete Bifurcation Analysis. In \textit{Doctoral Workshop on Mathematical and Engineering Methods in Computer Science}. 2017.

Detailed Information on Publication Record