J 2020

Parallel parameter synthesis algorithm for hybrid CTL

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

Základní údaje

Originální název

Parallel parameter synthesis algorithm for hybrid CTL

Autoři

BENEŠ, Nikola (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, domácí)

Vydání

Science of Computer Programming, 2020, 0167-6423

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

Impakt faktor

Impact factor: 0.863

Kód RIV

RIV/00216224:14330/20:00113986

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000499761400001

Klíčová slova anglicky

Parameter synthesis; Hybrid CTL; Parallelism; Model checking

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2021 07:54, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA18-00178S, projekt VaV
Ná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ů
LM2015055, projekt VaV
Název: Centrum pro systémovou biologii (Akronym: C4SYS)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, The national infrastructure C4SYS - Centre for Systems Biology
MUNI/A/1018/2018, interní kód MU
Ná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 MU
Ná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 MU
Ná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