Parallel parameter synthesis algorithm for hybrid CTL

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2020
Type Article in Periodical
Magazine / Source Science of Computer Programming
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1016/j.scico.2019.102321
Doi http://dx.doi.org/10.1016/j.scico.2019.102321
Keywords Parameter synthesis; Hybrid CTL; Parallelism; Model checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.