A Model Checking Approach to Discrete Bifurcation Analysis

• Autoři: BENEŠ Nikola; BRIM Luboš; DEMKO Martin; PASTVA Samuel; ŠAFRÁNEK David
• Rok publikování: 2016
• Druh: Článek ve sborníku
• Konference: Formal Methods. FM 2016
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/978-3-319-48989-6_6
• Obor: Informatika
• Klíčová slova: model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms; bifurcation analysis
• Popis: 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.

Související projekty

• Získávání parametrů biologických modelů pomocí techniky ověřování modelů
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.