Symbolic model checking of biochemical networks

Nathalie Chabrier; François Fages

doi:10.1007/3-540-36481-1_13

Symbolic model checking of biochemical networks

Nathalie Chabrier
, François Fages

INRIA Rocquencourt

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Model checking is an automatic method for deciding if a circuit or a program, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic such as CTL. In this paper we argue that symbolic model checking is feasible in systems biology and that it shows some advantages over simulation for querying and validating formal models of biological processes. We report our experiments on using the symbolic model checker NuSMV and the constraint-based model checker DMC, for the modeling and querying of two biological processes: a qualitative model of the mammalian cell cycle control after Kohn’s diagrams, and a quantitative model of gene expression regulation.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Corrado Priami
Publisher	Springer Verlag
Pages	149-162
Number of pages	14
ISBN (Print)	3540006052, 9783540006053
DOIs	https://doi.org/10.1007/3-540-36481-1_13
Publication status	Published - 1 Jan 2003
Externally published	Yes
Event	1st International Workshop on Computational Methods in Systems Biology, CMSB 2003 - Rovereto, Italy Duration: 24 Feb 2003 → 26 Feb 2003

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2602
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	1st International Workshop on Computational Methods in Systems Biology, CMSB 2003
Country/Territory	Italy
City	Rovereto
Period	24/02/03 → 26/02/03

Access to Document

10.1007/3-540-36481-1_13

Cite this

Chabrier, N., & Fages, F. (2003). Symbolic model checking of biochemical networks. In C. Priami (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 149-162). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2602). Springer Verlag. https://doi.org/10.1007/3-540-36481-1_13

Chabrier, Nathalie ; Fages, François. / Symbolic model checking of biochemical networks. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Corrado Priami. Springer Verlag, 2003. pp. 149-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{96557d9b5b0c4d93920a4deefb697e73,

title = "Symbolic model checking of biochemical networks",

abstract = "Model checking is an automatic method for deciding if a circuit or a program, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic such as CTL. In this paper we argue that symbolic model checking is feasible in systems biology and that it shows some advantages over simulation for querying and validating formal models of biological processes. We report our experiments on using the symbolic model checker NuSMV and the constraint-based model checker DMC, for the modeling and querying of two biological processes: a qualitative model of the mammalian cell cycle control after Kohn{\textquoteright}s diagrams, and a quantitative model of gene expression regulation.",

author = "Nathalie Chabrier and Fran{\c c}ois Fages",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2003.; 1st International Workshop on Computational Methods in Systems Biology, CMSB 2003 ; Conference date: 24-02-2003 Through 26-02-2003",

year = "2003",

month = jan,

day = "1",

doi = "10.1007/3-540-36481-1\_13",

language = "English",

isbn = "3540006052",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "149--162",

editor = "Corrado Priami",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

Chabrier, N & Fages, F 2003, Symbolic model checking of biochemical networks. in C Priami (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2602, Springer Verlag, pp. 149-162, 1st International Workshop on Computational Methods in Systems Biology, CMSB 2003, Rovereto, Italy, 24/02/03. https://doi.org/10.1007/3-540-36481-1_13

Symbolic model checking of biochemical networks. / Chabrier, Nathalie; Fages, François.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Corrado Priami. Springer Verlag, 2003. p. 149-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2602).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Symbolic model checking of biochemical networks

AU - Chabrier, Nathalie

AU - Fages, François

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2003.

PY - 2003/1/1

Y1 - 2003/1/1

N2 - Model checking is an automatic method for deciding if a circuit or a program, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic such as CTL. In this paper we argue that symbolic model checking is feasible in systems biology and that it shows some advantages over simulation for querying and validating formal models of biological processes. We report our experiments on using the symbolic model checker NuSMV and the constraint-based model checker DMC, for the modeling and querying of two biological processes: a qualitative model of the mammalian cell cycle control after Kohn’s diagrams, and a quantitative model of gene expression regulation.

AB - Model checking is an automatic method for deciding if a circuit or a program, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic such as CTL. In this paper we argue that symbolic model checking is feasible in systems biology and that it shows some advantages over simulation for querying and validating formal models of biological processes. We report our experiments on using the symbolic model checker NuSMV and the constraint-based model checker DMC, for the modeling and querying of two biological processes: a qualitative model of the mammalian cell cycle control after Kohn’s diagrams, and a quantitative model of gene expression regulation.

UR - https://www.scopus.com/pages/publications/84958602011

U2 - 10.1007/3-540-36481-1_13

DO - 10.1007/3-540-36481-1_13

M3 - Conference contribution

AN - SCOPUS:84958602011

SN - 3540006052

SN - 9783540006053

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 149

EP - 162

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Priami, Corrado

PB - Springer Verlag

T2 - 1st International Workshop on Computational Methods in Systems Biology, CMSB 2003

Y2 - 24 February 2003 through 26 February 2003

ER -

Chabrier N, Fages F. Symbolic model checking of biochemical networks. In Priami C, editor, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2003. p. 149-162. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-36481-1_13

Symbolic model checking of biochemical networks

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this