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; Luboš BRIM; Martin DEMKO ; Samuel PASTVA and David ŠAFRÁNEK

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

Proceedings paper

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

Marked to be transferred to RIV

Yes

RIV identification code

RIV/00216224:14330/16:00088309

Organization unit

Faculty of Informatics

ISBN

978-3-319-48988-9

ISSN

Keywords in English

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

Abstract

In the original language

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

Cite

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://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 = {https://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  - CONF
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://doi.org/10.1007/978-3-319-48989-6\_{}6.

Přehled o publikaci