A Model Checking Approach to Discrete Bifurcation Analysis

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088309" target="_blank" >RIV/00216224:14330/16:00088309 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-48989-6_6" target="_blank" >http://dx.doi.org/10.1007/978-3-319-48989-6_6</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-48989-6_6" target="_blank" >10.1007/978-3-319-48989-6_6</a>

Jazyk výsledku

angličtina

Název v původním jazyce

A Model Checking Approach to Discrete Bifurcation Analysis

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

A Model Checking Approach to Discrete Bifurcation Analysis

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA15-11089S" target="_blank" >GA15-11089S: Získávání parametrů biologických modelů pomocí techniky ověřování modelů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Formal Methods. FM 2016

ISBN

9783319489889

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

85-101

Název nakladatele

Springer International Publishing

Místo vydání

Neuveden

Místo konání akce

Limassol, Cyprus

Datum konání akce

7. 11. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—