Parameter Synthesis by Parallel Coloured CTL Model Checking

D 2015

Parameter Synthesis by Parallel Coloured CTL Model Checking

BRIM, Luboš, Milan ČEŠKA, Martin DEMKO, Samuel PASTVA, David ŠAFRÁNEK et. al.

Basic information

Original name

Parameter Synthesis by Parallel Coloured CTL Model Checking

Authors

BRIM, Luboš (203 Czech Republic, belonging to the institution), Milan ČEŠKA (203 Czech Republic, belonging to the institution), Martin DEMKO (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Neuveden, Computational Methods in Systems Biology, p. 251-263, 13 pp. 2015

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

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í

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00081130

Organization unit

Faculty of Informatics

ISBN

978-3-319-23400-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-23401-4_21

UT WoS

000366198300021

Keywords in English

model checking; systems biology; Computational Tree Logic; dynamical systems; distributed algorithms

Abstract

V originále

We propose a new distributed-memory parallel algorithm for parameter synthesis from CTL hypotheses. The algorithm colours the state space transitions by different parameterisations and extends CTL model checking to identify the maximal set of parameters that guarantee the satisfaction of the given CTL property. We experimentally confirm good scalability of our approach and demonstrate its applicability in the case study of a genetic switch controlling decisions in the cell cycle.

Links

GA15-11089S, research and development project

Name: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Czech Science Foundation

MUNI/A/1159/2014, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masaryk University, Category A

MUNI/A/1206/2014, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BRIM, Luboš, Milan ČEŠKA, Martin DEMKO, Samuel PASTVA and David ŠAFRÁNEK. Parameter Synthesis by Parallel Coloured CTL Model Checking. In Roux, Olivier and Bourdon, Jérémie. Computational Methods in Systems Biology. Neuveden: Springer International Publishing, 2015, p. 251-263. ISBN 978-3-319-23400-7. Available from: https://dx.doi.org/10.1007/978-3-319-23401-4_21.

@inproceedings{1314024,
   author = {Brim, Luboš and Češka, Milan and Demko, Martin and Pastva, Samuel and Šafránek, David},
   address = {Neuveden},
   booktitle = {Computational Methods in Systems Biology},
   doi = {http://dx.doi.org/10.1007/978-3-319-23401-4_21},
   editor = {Roux, Olivier and Bourdon, Jérémie},
   keywords = {model checking; systems biology; Computational Tree Logic; dynamical systems; distributed algorithms},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-23400-7},
   pages = {251-263},
   publisher = {Springer International Publishing},
   title = {Parameter Synthesis by Parallel Coloured CTL Model Checking},
   year = {2015}
}

TY  - JOUR
ID  - 1314024
AU  - Brim, Luboš - Češka, Milan - Demko, Martin - Pastva, Samuel - Šafránek, David
PY  - 2015
TI  - Parameter Synthesis by Parallel Coloured CTL Model Checking
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319234007
KW  - model checking
KW  - systems biology
KW  - Computational Tree Logic
KW  - dynamical systems
KW  - distributed algorithms
N2  - We propose a new distributed-memory parallel algorithm for parameter synthesis from CTL hypotheses. The algorithm colours the state space transitions by different parameterisations and extends CTL model checking to identify the maximal set of parameters that guarantee the satisfaction of the given CTL property. We experimentally confirm good scalability of our approach and demonstrate its applicability in the case study of a genetic switch controlling decisions in the cell cycle.
ER  -

BRIM, Luboš, Milan ČEŠKA, Martin DEMKO, Samuel PASTVA and David ŠAFRÁNEK. Parameter Synthesis by Parallel Coloured CTL Model Checking. In Roux, Olivier and Bourdon, Jérémie. \textit{Computational Methods in Systems Biology}. Neuveden: Springer International Publishing, 2015, p.~251-263. ISBN~978-3-319-23400-7. Available from: https://dx.doi.org/10.1007/978-3-319-23401-4\_{}21.

Detailed Information on Publication Record