J 2020

Parallel parameter synthesis algorithm for hybrid CTL

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK

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

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

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

References:

Impact factor

Impact factor: 0.863

RIV identification code

RIV/00216224:14330/20:00113986

Organization unit

Faculty of Informatics

DOI

UT WoS

000499761400001

Keywords in English

Parameter synthesis; Hybrid CTL; Parallelism; Model checking

Tags

International impact, Reviewed
Změněno: 29/4/2021 07:54, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

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 project
Name: Diskrétní bifurkační analýza reaktivních systémů
Investor: Czech Science Foundation
LM2015055, research and development project
Name: Centrum pro systémovou biologii (Acronym: C4SYS)
Investor: Ministry of Education, Youth and Sports of the CR
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