Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. In Rupak Majumdar and Viktor Kunčak. Computer Aided Verification. CAV 2017. LNCS 10426. Cham: Springer International Publishing, 2017, s. 591-598. ISBN 978-3-319-63386-2. Dostupné z: https://dx.doi.org/10.1007/978-3-319-63387-9_29.

Základní údaje

Originální název

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, garant, domácí), Martin DEMKO (703 Slovensko, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, domácí)

Vydání

LNCS 10426. Cham, Computer Aided Verification. CAV 2017, od s. 591-598, 8 s. 2017

Nakladatel

Springer International Publishing

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/17:00094898

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-63386-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-63387-9_29

UT WoS

000432196400029

Klíčová slova anglicky

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

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We present a novel tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic. The tool is based on the algorithm of parallel semi-symbolic coloured model checking that extends standard model checking methods to cope with parametrised Kripke structures. The tool implements state-of-the-art techniques developed in our previous research and is primarily intended to be used for the analysis of dynamical systems with uncertain parameters that frequently arise in computational systems biology. However, it can be employed for any dynamical system where the non-linear equations can be sufficiently well approximated by piecewise multi-affine equations.

---

Návaznosti

GA15-11089S, projekt VaV	Název: Získávání parametrů biologických modelů pomocí techniky ověřování modelů Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů
LM2015055, projekt VaV	Název: Centrum pro systémovou biologii (Akronym: C4SYS) Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, The national infrastructure C4SYS - Centre for Systems Biology
MUNI/A/0897/2016, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0992/2016, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty