@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)",
}