Parallel parameter synthesis algorithm for hybrid CTL

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Parallel parameter synthesis algorithm for hybrid CTL. Science of Computer Programming. 2020, roč. 185, č. 102321, s. 1-19. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2019.102321.

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

URL

Impakt faktor

Impact factor: 0.863

Kód RIV

RIV/00216224:14330/20:00113986

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1016/j.scico.2019.102321

UT WoS

000499761400001

Klíčová slova anglicky

Parameter synthesis; Hybrid CTL; Parallelism; Model checking

Příznaky

Mezinárodní význam, Recenzováno

---

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