Parallel parameter synthesis algorithm for hybrid CTL

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BENEŠ Nikola BRIM Luboš PASTVA Samuel ŠAFRÁNEK David
Rok publikování	2020
Druh	Článek v odborném periodiku
Časopis / Zdroj	Science of Computer Programming
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1016/j.scico.2019.102321
Doi	http://dx.doi.org/10.1016/j.scico.2019.102321
Klíčová slova	Parameter synthesis; Hybrid CTL; Parallelism; Model checking
Popis	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.
Související projekty:	The national infrastructure C4SYS - Centre for Systems Biology Diskrétní bifurkační analýza reaktivních systémů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII. Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20