BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA and 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. p. 591-598. ISBN 978-3-319-63386-2. doi:10.1007/978-3-319-63387-9_29. 2017.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, guarantor, belonging to the institution), Martin DEMKO (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, belonging to the institution).
Edition LNCS 10426. Cham, Computer Aided Verification. CAV 2017, p. 591-598, 8 pp. 2017.
Publisher Springer International Publishing
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/17:00094898
Organization unit Faculty of Informatics
ISBN 978-3-319-63386-2
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-63387-9_29
UT WoS 000432196400029
Keywords in English model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
Tags core_A, firank_1
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:18.
Abstract
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.
Links
GA15-11089S, research and development projectName: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Czech Science Foundation
LM2015055, research and development projectName: Centrum pro systémovou biologii (Acronym: C4SYS)
Investor: Ministry of Education, Youth and Sports of the CR
MUNI/A/0897/2016, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masaryk University, Category A
MUNI/A/0992/2016, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 19/4/2024 12:48