Symbolic Model Checking of Biochemical Networks Export

@incollection{citeulike:5023037, 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.}, author = {Chabrier, Nathalie and Fages, Fran\c{c}ois}, citeulike-article-id = {5023037}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-36481-1_13}, citeulike-linkout-1 = {http://www.springerlink.com/content/9931wm66mn4835x7}, doi = {10.1007/3-540-36481-1_13}, journal = {Computational Methods in Systems Biology}, keywords = {biological-machines, biological-networks, biological-structures, biological-systems, formal-biology, formal-development, formal-methods, formal-theories, logical-frameworks, logical-structures, logical-systems, logical-theories, model-checkers, model-checking, systems-biology}, pages = {149--162}, posted-at = {2009-06-30 15:25:56}, priority = {2}, title = {Symbolic Model Checking of Biochemical Networks}, url = {http://dx.doi.org/10.1007/3-540-36481-1_13}, year = {2003} }

TY - CHAP ID - citeulike:5023037 L3 - citeulike-article-id:5023037 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. JF - Computational Methods in Systems Biology EP - 162 TI - Symbolic Model Checking of Biochemical Networks SP - 149 KW - biological-machines KW - biological-networks KW - biological-structures KW - biological-systems KW - formal-biology KW - formal-development KW - formal-methods KW - formal-theories KW - logical-frameworks KW - logical-structures KW - logical-systems KW - logical-theories KW - model-checkers KW - model-checking KW - systems-biology AU - Chabrier, Nathalie AU - Fages, François PY - 2003/// UR - http://dx.doi.org/10.1007/3-540-36481-1_13 ER -