BENEŠ, Nikola, Luboš BRIM, Martin GELETKA, Samuel PASTVA and David ŠAFRÁNEK. Accelerating Parameter Synthesis Using Semi-algebraic Constraints. Online. In Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth. Integrated Formal Methods. LNCS 11918. Cham: Springer International Publishing, 2019, p. 27-45. ISBN 978-3-030-34967-7. Available from: https://dx.doi.org/10.1007/978-3-030-34968-4_2.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Accelerating Parameter Synthesis Using Semi-algebraic Constraints
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Martin GELETKA (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 11918. Cham, Integrated Formal Methods, p. 27-45, 19 pp. 2019.
Publisher Springer International Publishing
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/19:00108262
Organization unit Faculty of Informatics
ISBN 978-3-030-34967-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-34968-4_2
UT WoS 000611734300002
Keywords in English parameter synthesis; semi-algebraic set; CTL
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 15/4/2021 12:06.
Abstract
We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.
Links
GA18-00178S, research and development projectName: Diskrétní bifurkační analýza reaktivních systémů
Investor: Czech Science Foundation
PrintDisplayed: 13/5/2024 05:57