BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA and David ŠAFRÁNEK. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. In Cyrille Artho et al. Automated Technology for Verification and Analysis. ATVA 2016. LNCS 9938. Neuveden: Springer International Publishing, 2016, p. 192-208. ISBN 978-3-319-46519-7. Available from: https://dx.doi.org/10.1007/978-3-319-46520-3_13.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, 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, guarantor, belonging to the institution).
Edition LNCS 9938. Neuveden, Automated Technology for Verification and Analysis. ATVA 2016, p. 192-208, 17 pp. 2016.
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"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/16:00088098
Organization unit Faculty of Informatics
ISBN 978-3-319-46519-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-46520-3_13
UT WoS 000389808100013
Keywords in English model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
Tags core_A, firank_A
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:15.
Abstract
We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.
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
MUNI/A/0945/2015, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
PrintDisplayed: 23/7/2024 02:36