BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK. Parallel parameter synthesis algorithm for hybrid CTL. Science of Computer Programming. 2020, vol. 185, No 102321, p. 1-19. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2019.102321.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Parallel parameter synthesis algorithm for hybrid CTL
Authors BENEŠ, Nikola (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, belonging to the institution).
Edition Science of Computer Programming, 2020, 0167-6423.
Other information
Original language English
Type of outcome Article in a journal
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
WWW URL
Impact factor Impact factor: 0.863
RIV identification code RIV/00216224:14330/20:00113986
Organization unit Faculty of Informatics
Doi http://dx.doi.org/10.1016/j.scico.2019.102321
UT WoS 000499761400001
Keywords in English Parameter synthesis; Hybrid CTL; Parallelism; Model checking
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2021 07:54.
Abstract
Parametrised models of dynamical systems arise in various areas of science. In this work, we focus on models described as parametrised Kripke structures with properties formulated in a hybrid extension of the Computation Tree Logic. Our goal is to identify all the parametrisations under which the given model satisfies the properties. To that end, we propose a novel semi-symbolic parallel parameter synthesis algorithm. The algorithm is built on top of an existing approach that utilises the so-called Extended Dependency Graphs. We extend this approach to deal with parameters. To demonstrate the usefulness of our approach, we show its application to several case studies taken from systems biology.
Links
GA18-00178S, research and development projectName: Diskrétní bifurkační analýza reaktivních systémů
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/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: 23/7/2024 02:36