What is a Cell Cycle Checkpoint? The TotemBioNet Answer

Abstract

TotemBioNet is a new software platform to assist the design of qualitative regulatory network models by combining “genetically modified Hoare logic”, temporal logic model checking and optimized enumeration techniques. TotemBioNet is particularly efficient to manage parameter identification, the most critical step of formal modelling. It is also remarkably flexible and efficient to check properties in order to explore biological assumptions. To illustrate this efficacy, we address the classical example of the cell cycle, where the passage from one phase to the next one, called checkpoint, is crucial but is usually a rather fuzzy informal concept. The cyclic behaviour of the cell cycle is specified by temporal logic and the order of individual events inside each phase is explored thanks to quantifiers introduced in Hoare logic. This way, TotemBioNet rapidly suggests a sensible formalization of the notion of checkpoint.