Abstract
Biologists use diagrams to represent interactions between molecular species, and on the computer, diagrammatic notations are also employed in interactive maps. These diagrams are fundamentally of two types: reaction graphs and activation/inhibition graphs. In this tutorial, we study these graphs with formal methods originating from programming theory. We consider systems of biochemical reactions with kinetic expressions, as written in the Systems Biology Markup Language (SBML), and interpreted in the Biochemical Abstract Machine (Biocham) at different levels of abstraction, by either an asynchronous boolean transition system, a continuous time Markov chain, or a system of Ordinary Differential Equations over molecular concentrations. We show that under general conditions satisfied in practice, the activation/inhibition graph is independent of the precise kinetic expressions, and is computable in linear time in the number of reactions. Then we consider the formalization of the biological properties of systems, as observed in experiments, in temporal logics. We show that these logics are expressive enough to capture semi-qualitative semi-quantitative properties of the boolean and differential semantics of reaction models, and that model-checking techniques can be used to validate a model w.r.t. its temporal specification, complete it, and search for kinetic parameter values. We illustrate this modelling method with examples on the MAPK signalling cascade, and on Kohn’s map of the mammalian cell cycle.

URL:
http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2008-024

BibTeX:

@inproceedings{REWERSE-RP-2008-024,
	author = {Fran\c{c}ois Fages and Sylvain Soliman},
	title = {Formal Cell Biology in Biocham},
	booktitle = {Proceedings of 8th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Computational Systems Biology, Bertinoro, Italy (2nd--7th June 2008)},
	year = {2008},
	volume = {5016},
	series = {LNCS},
	pages = {54--80},
	url = {http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2008-024}
}