Title: Algorithmic Algebraic Model Checking I: The Case of Biochemical Systems and their Reachability Analysis

(NYU-CS-TR859)

Author:  C. Piazza, M. Antoniotto, V. Mysore, A. Policriti, F. Winkler, B. Mishra.

Abstract:
Presently, there is no clear way to determine if the current body of
biological facts is sufficient to explain phenomenology. 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. The approaches
developed by control theorists analyzing stability of a system with 
feedback, physicists studying asymptotic properties of dynamical
systems, computer scientists reasoning about discrete or hybrid
(combining discrete events with continuous events) reactive
systems---all have tried to address some aspects of the same problem
in a very concrete manner. We explore here how biological processes
could be studied in a similar manner, and how the appropriate tools
for this purpose can be created.

In this paper, we suggest a possible confluence of the theory of
hybrid automata and the techniques of algorithmic algebra to create a
computational basis for systems biology. We start by discussing our
basis for this choice -- semi-algebraic hybrid systems, as we also recognize its power and
limitations. We explore solutions to the bounded-reachability
problem through symbolic computation methods, applied to the
descriptions of the traces of the hybrid automaton. Because the
description of the automaton is through semi-algebraic sets, the
evolution of the automaton can be described even in cases where system
parameters and initial conditions are unspecified. Nonetheless,
semialgebraic decision procedures provide a succinct description of
algebraic constraints over the initial values and parameters 
for which proper behavior of the system can be expected. In addition,
by keeping track of conservation principles 
in terms of constraint or invariant manifolds on which the system must
evolve, we avoid many of the obvious pitfalls of numerical approaches.