Exploring Parameter Space of Stochastic Biochemical Systems
Using Quantitative Model Checking

D 2013

Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking

BRIM, Luboš; Milan ČEŠKA; Sven DRAŽAN and David ŠAFRÁNEK

Basic information

Original name

Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking

Authors

BRIM, Luboš (203 Czech Republic, belonging to the institution); Milan ČEŠKA (203 Czech Republic, belonging to the institution); Sven DRAŽAN (203 Czech Republic, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Berlin, 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, p. 107-123, 17 pp. 2013

Publisher

Springer Berlin Heidelberg

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066280

Organization unit

Faculty of Informatics

ISBN

978-3-642-39798-1

ISSN

DOI

https://doi.org/10.1007/978-3-642-39799-8_7

Keywords in English

continuous-time Markov chains; parameter exploration; model checking

Abstract

In the original language

We propose an automated method for exploring kinetic parameters of stochastic biochemical systems. The main question addressed is how the validity of an a priori given hypothesis expressed as a temporal logic property depends on kinetic parameters. Our aim is to compute a landscape function that, for each parameter point from the inspected parameter space, returns the quantitative model checking result for the respective continuous time Markov chain. Since the parameter space is in principle dense, it is infeasible to compute the landscape function directly. Hence, we design an effective method that iteratively approximates the lower and upper bounds of the landscape function with respect to a given accuracy. To this end, we modify the standard uniformization technique and introduce an iterative parameter space decomposition. We also demonstrate our approach on two biologically motivated case studies.

Links

EE2.3.20.0256, research and development project

Name: Vytvoření výzkumného týmu a mezinárodního konzorcia pro počítačový model buňky sinice

EE2.3.30.0009, research and development project

Name: Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci

GAP202/11/0312, research and development project

Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)

Investor: Czech Science Foundation

MUNI/A/0739/2012, interní kód MU

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

Investor: Masaryk University, Category A

MUNI/A/0760/2012, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)

Investor: Masaryk University, Category A

Cite

BRIM, Luboš; Milan ČEŠKA; Sven DRAŽAN and David ŠAFRÁNEK. Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. In 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Berlin: Springer Berlin Heidelberg, 2013, p. 107-123. ISBN 978-3-642-39798-1. Available from: https://doi.org/10.1007/978-3-642-39799-8_7.

@inproceedings{1119886,
   author = {Brim, Luboš and Češka, Milan and Dražan, Sven and Šafránek, David},
   address = {Berlin},
   booktitle = {25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
   doi = {https://doi.org/10.1007/978-3-642-39799-8_7},
   keywords = {continuous-time Markov chains; parameter exploration; model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin},
   isbn = {978-3-642-39798-1},
   pages = {107-123},
   publisher = {Springer Berlin Heidelberg},
   title = {Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking},
   url = {http://link.springer.com/chapter/10.1007%2F978-3-642-39799-8_7},
   year = {2013}
}

TY  - CONF
ID  - 1119886
AU  - Brim, Luboš - Češka, Milan - Dražan, Sven - Šafránek, David
PY  - 2013
TI  - Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking
PB  - Springer Berlin Heidelberg
CY  - Berlin
SN  - 9783642397981
KW  - continuous-time Markov chains
KW  - parameter exploration
KW  - model checking
UR  - http://link.springer.com/chapter/10.1007%2F978-3-642-39799-8_7
N2  - We propose an automated method for exploring kinetic parameters of stochastic biochemical systems. The main question addressed is how the validity of an a priori given hypothesis expressed as a temporal logic property depends on kinetic parameters. Our aim is to compute a landscape function that, for each parameter point from the inspected parameter space, returns the quantitative model checking result for the respective continuous time Markov chain. Since the parameter space is in principle dense, it is infeasible to compute the landscape function directly. Hence, we design an effective method that iteratively approximates the lower and upper bounds of the landscape function with respect to a given accuracy. To this end, we modify the standard uniformization technique and introduce an iterative parameter space decomposition. We also demonstrate our approach on two biologically motivated case studies.
ER  -

BRIM, Luboš; Milan ČEŠKA; Sven DRAŽAN and David ŠAFRÁNEK. Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. In \textit{25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings}. Berlin: Springer Berlin Heidelberg, 2013, p.~107-123. ISBN~978-3-642-39798-1. Available from: https://doi.org/10.1007/978-3-642-39799-8\_{}7.

Přehled o publikaci