BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA a Matej HAJNAL. Model Checking Approach to Discrete Bifurcation Analysis. Online. In Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2017, [citováno 2024-04-23]
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Model Checking Approach to Discrete Bifurcation Analysis
Autoři BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA a Matej HAJNAL
Vydání Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2017.
Další údaje
Originální jazyk angličtina
Typ výsledku Prezentace na konferencích
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW URL
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky model checking, bifurcation analysis, parameters, phase portrait, temporal logic
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Martin Demko, Ph.D., učo 325073. Změněno: 4. 9. 2018 12:05.
Anotace
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.
Návaznosti
GA15-11089S, projekt VaVNázev: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů
LM2015055, projekt VaVNázev: Centrum pro systémovou biologii (Akronym: C4SYS)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, The national infrastructure C4SYS - Centre for Systems Biology
MUNI/A/0945/2015, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 23. 4. 2024 18:11