We describe an efficient procedure for proving
stabilization of biological systems modeled
as qualitative networks or genetic regulatory networks.
For scalability, our procedure
uses modular proof techniques, where state-space exploration
is applied only locally to small pieces of the system rather than
the entire system as a whole.
Our procedure exploits the observation that, in practice, the form of
modular proofs
can be restricted to a very limited set.
For completeness, our technique falls back on a non-compositional counterexample search.
Using our new procedure, we have solved a number of challenging
published examples, including:
a 3-D model of the mammalian epidermis;
a model of metabolic networks operating in type-2 diabetes;
a model of fate determination of vulval precursor cells in the
C. elegans worm;
and a model of pair-rule regulation during segmentation
in the Drosophila embryo.
Our results show many orders
of magnitude speedup in cases where previous stabilization proving techniques
were known to
succeed, and new results in cases where tools had previously failed.