CIMS-TR 2005-859 Algorithmic Algebraic Model Checking I: The Case of Biochemical Systems and their Reachability Analysis ?

Abstract

Presently, there is no clear way to determine if the current body of biological facts is sufficient to explain phenomenology. In the biological community, it is not uncommon to assume certain biological problems to have achieved a cognitive finality without rigorous justification. In these particular cases, rigorous mathematical models with automated tools for reasoning, simulation, and computation can be of enormous help to uncover cognitive flaws, qualitative simplification or overly generalized assumptions. Some ideal candidates for such study would include: prion hypothesis, cell cycle machinery (DNA replication and repair, chromosome segregation, cell-cycle period control, spindle pole duplication, etc.), muscle contractility, processes involved in cancer (cell cycle regulation, angiogenesis, DNA repair, apoptosis, cellular senescence, tissue space modeling enzymes, etc.), signal transduction pathways, circadian rhythms (especially the effect of small molecular concentration on its robustness), and many others. Fortunately, similar issues had been tackled in the past by other disciplines: for instance, design of complex microprocessors involving many millions of transistors, building and controlling configurable robots involving very high degreeof-freedom actuators, implementing hybrid controllers for highway traffic or airtraffic, or even reasoning about data traffic on a computer network. The approaches developed by control theorists analyzing stability of a system with