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.

Basic information

Original name

A Model Checking Approach to Discrete Bifurcation Analysis

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Martin DEMKO (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

LNCS 9995. Neuveden, Formal Methods. FM 2016, p. 85-101, 17 pp. 2016

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

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í

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00088309

Organization unit

Faculty of Informatics

ISBN

978-3-319-48988-9

ISSN

DOI

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

UT WoS

000389793300006

Keywords in English

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

Abstract

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.

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

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, Samuel PASTVA and 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, p. 85-101. ISBN 978-3-319-48988-9. Available from: 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 and 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, p.~85-101. ISBN~978-3-319-48988-9. Available from: https://dx.doi.org/10.1007/978-3-319-48989-6\_{}6.

Detailed Information on Publication Record