ŠMIJÁKOVÁ, Eva, Samuel PASTVA, David ŠAFRÁNEK and Luboš BRIM. Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications. (Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications). Online. In Abate A., Petrov T., Wolf V. Computational Methods in Systems Biology. CMSB 2020. Lecture Notes in Computer Science, vol 12314. Cham: Springer, Cham, 2020, p. 280-297. ISBN 978-3-030-60326-7. Available from: https://dx.doi.org/10.1007/978-3-030-60327-4_15.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications.
Authors ŠMIJÁKOVÁ, Eva (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution), David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution) and Luboš BRIM (203 Czech Republic, belonging to the institution).
Edition Cham, Computational Methods in Systems Biology. CMSB 2020. Lecture Notes in Computer Science, vol 12314, p. 280-297, 18 pp. 2020.
Publisher Springer, Cham
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
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/20:00114364
Organization unit Faculty of Informatics
ISBN 978-3-030-60326-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-60327-4_15
Keywords in English Hybrid systems; Parameter synthesis; Rectangular abstraction; Semi-symbolic; Hybrid CTL
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 8/2/2024 10:05.
Abstract
We consider the parameter synthesis problem for multi-affine hybrid systems and properties specified using a hybrid extension of CTL (HCTL). The goal is to determine the sets of parameter valuations for which the given hybrid system satisfies the desired HCTL property. As our main contribution, we propose a shared-memory parallel algorithm which efficiently computes such parameter valuation sets. We combine a rectangular discretisation of the continuous dynamics with the discrete transitions of the hybrid system to obtain a single over-approximating semi-symbolic transition system. Such system can be then analysed using a fixed-point parameter synthesis algorithm to obtain all satisfying parametrisations. We evaluate the scalability of the method and demonstrate its applicability in a biological case study.
Links
GA18-00178S, research and development projectName: Diskrétní bifurkační analýza reaktivních systémů
Investor: Czech Science Foundation
MUNI/A/1018/2018, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masaryk University, Category A
MUNI/A/1050/2019, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Acronym: SV-FI MAV IX)
Investor: Masaryk University, Category A
MUNI/A/1076/2019, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 22/6/2024 06:34