Parallel Parameter Synthesis for Multi-affine Hybrid Systems
from Hybrid CTL Specifications.

D 2020

Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications.

ŠMIJÁKOVÁ, Eva, Samuel PASTVA, David ŠAFRÁNEK and Luboš BRIM

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

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

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

Abstract

V originále

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 project

Name: Diskrétní bifurkační analýza reaktivních systémů

Investor: Czech Science Foundation

MUNI/A/1018/2018, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masaryk University, Category A

MUNI/A/1050/2019, interní kód MU

Name: 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 MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

Š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.

@inproceedings{1685211,
   author = {Šmijáková, Eva and Pastva, Samuel and Šafránek, David and Brim, Luboš},
   address = {Cham},
   booktitle = {Computational Methods in Systems Biology. CMSB 2020. Lecture Notes in Computer Science, vol 12314},
   doi = {http://dx.doi.org/10.1007/978-3-030-60327-4_15},
   editor = {Abate A., Petrov T., Wolf V.},
   keywords = {Hybrid systems; Parameter synthesis; Rectangular abstraction; Semi-symbolic; Hybrid CTL},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-60326-7},
   pages = {280-297},
   publisher = {Springer, Cham},
   title = {Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications.},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-60327-4_15},
   year = {2020}
}

TY  - JOUR
ID  - 1685211
AU  - Šmijáková, Eva - Pastva, Samuel - Šafránek, David - Brim, Luboš
PY  - 2020
TI  - Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications.
PB  - Springer, Cham
CY  - Cham
SN  - 9783030603267
KW  - Hybrid systems
KW  - Parameter synthesis
KW  - Rectangular abstraction
KW  - Semi-symbolic
KW  - Hybrid CTL
UR  - https://link.springer.com/chapter/10.1007/978-3-030-60327-4_15
N2  - 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.
ER  -

Š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. \textit{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.

Detailed Information on Publication Record