ŠMIJÁKOVÁ, Eva, Samuel PASTVA, David ŠAFRÁNEK a Luboš BRIM. 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, s. 280-297. ISBN 978-3-030-60326-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-60327-4_15.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications.
Autoři ŠMIJÁKOVÁ, Eva (703 Slovensko, domácí), Samuel PASTVA (703 Slovensko, domácí), David ŠAFRÁNEK (203 Česká republika, garant, domácí) a Luboš BRIM (203 Česká republika, domácí).
Vydání Cham, Computational Methods in Systems Biology. CMSB 2020. Lecture Notes in Computer Science, vol 12314, od s. 280-297, 18 s. 2020.
Nakladatel Springer, Cham
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/20:00114364
Organizační jednotka Fakulta informatiky
ISBN 978-3-030-60326-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-60327-4_15
Klíčová slova anglicky Hybrid systems; Parameter synthesis; Rectangular abstraction; Semi-symbolic; Hybrid CTL
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. David Šafránek, Ph.D., učo 3159. Změněno: 8. 2. 2024 10:05.
Anotace
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.
Návaznosti
GA18-00178S, projekt VaVNázev: Diskrétní bifurkační analýza reaktivních systémů
Investor: Grantová agentura ČR, Diskrétní bifurkační analýza reaktivních systémů
MUNI/A/1018/2018, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1050/2019, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1076/2019, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 7. 5. 2024 14:02