A Model Checking Approach to Discrete Bifurcation Analysis

D 2016

A Model Checking Approach to Discrete Bifurcation Analysis

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

Základní údaje

Originální název

A Model Checking Approach to Discrete Bifurcation Analysis

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Martin DEMKO (703 Slovensko, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, garant, domácí)

Vydání

LNCS 9995. Neuveden, Formal Methods. FM 2016, od s. 85-101, 17 s. 2016

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088309

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-48988-9

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-48989-6_6

UT WoS

000389793300006

Klíčová slova anglicky

model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms; bifurcation analysis

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 19:12, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA15-11089S, projekt VaV

Ná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ů

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

Ná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

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. A Model Checking Approach to Discrete Bifurcation Analysis. In John S. Fitzgerald et al. Formal Methods. FM 2016. LNCS 9995. Neuveden: Springer International Publishing, 2016, s. 85-101. ISBN 978-3-319-48988-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-48989-6_6.

@inproceedings{1359653,
   author = {Beneš, Nikola and Brim, Luboš and Demko, Martin and Pastva, Samuel and Šafránek, David},
   address = {Neuveden},
   booktitle = {Formal Methods. FM 2016},
   doi = {http://dx.doi.org/10.1007/978-3-319-48989-6_6},
   edition = {LNCS 9995},
   editor = {John S. Fitzgerald et al.},
   keywords = {model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms; bifurcation analysis},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-48988-9},
   pages = {85-101},
   publisher = {Springer International Publishing},
   title = {A Model Checking Approach to Discrete Bifurcation Analysis},
   year = {2016}
}

TY  - JOUR
ID  - 1359653
AU  - Beneš, Nikola - Brim, Luboš - Demko, Martin - Pastva, Samuel - Šafránek, David
PY  - 2016
TI  - A Model Checking Approach to Discrete Bifurcation Analysis
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319489889
KW  - model checking
KW  - satisfiability modulo theories
KW  - Computational Tree Logic
KW  - dynamical systems
KW  - distributed algorithms
KW  - bifurcation analysis
N2  - 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.
ER  -

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. A Model Checking Approach to Discrete Bifurcation Analysis. In John S. Fitzgerald et al. \textit{Formal Methods. FM 2016}. LNCS 9995. Neuveden: Springer International Publishing, 2016, s.~85-101. ISBN~978-3-319-48988-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-48989-6\_{}6.

Podrobný výpis o publikaci