Informační systém Masarykovy univerzity 

A Model Checking Approach to Discrete Bifurcation Analysis

česky | in English

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, 17 s. ISBN 978-3-319-48988-9. doi:10.1007/978-3-319-48989-6_6.
Další formáty:   BibTeX LaTeX RIS
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
Originální jazyk angličtina
Typ výsledku Článek ve sborníku
Obor Informatika
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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-48989-6_6
Klíčová slova anglicky model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms; bifurcation analysis
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2017 06:57.
Anotace
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 VaVNázev: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/0945/2015, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 20. 9. 2017 23:45

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 20. 9. 2017 23:45, 38. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému