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, 8 s. ISBN 978-3-319-63386-2. doi:10.1007/978-3-319-63387-9_29.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-63387-9_29
Klíčová slova anglicky model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
Štítky firank_1
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 26. 2. 2018 12:31.
Anotace
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 VaVNázev: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Grantová agentura ČR, Standardní projekty
LM2015055, projekt VaVNázev: Centrum pro systémovou biologii (Akronym: C4SYS)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Velké infrastruktury pro výzkum, vývoj a inovace
MUNI/A/0897/2016, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0992/2016, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 18. 1. 2020 23:54