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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Presentations at conferences
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
WWW URL
Organization unit Faculty of Informatics
Keywords in English model checking, bifurcation analysis, parameters, phase portrait, temporal logic
Tags International impact, Reviewed
Changed by Changed by: RNDr. Martin Demko, Ph.D., učo 325073. Changed: 4/9/2018 12:05.
Abstract
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 projectName: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Czech Science Foundation
LM2015055, research and development projectName: Centrum pro systémovou biologii (Acronym: C4SYS)
Investor: Ministry of Education, Youth and Sports of the CR
MUNI/A/0945/2015, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
PrintDisplayed: 19/7/2024 01:42