Proving stabilization of biological systems

BioCheck is a tool that proves stabilization of systems represented as Qualitative Networks (synchronous) or Genetic Regulatory Netoworks (asynchronous). Such networks consist of n processes, each encapsulating a single integer variable that represents a certain modelled biological entity. The variables are updated following a function that depends on other variables and is specific to the biological entity modelled.

The BioCheck prover performs a guided search for chains of local reasoning of the form:

FG(φ₁) ∧ FG(φ₂) ∧ ... ∧ FG(φ_m) ⇒ FG(ψ), where φ_i are simple formulas (inequalities) about the input variables of a component and φ is a similar simple formula about the output variable. The huge state space (4²⁵ for small models, 4⁶⁰⁰ for a 3-D skin model) is never generated.

Downloads

• Tool release (benchmark input files included):
  BioCheck-1.3.zip (224K) 18 Apr 2010 (bug fixes)
  BioCheck-1.2.zip (216K) 09 Dec 2010 (bug fixes)
  BioCheck-1.1.zip (216K) 17 Nov 2010 (bug fixes)
  BioCheck-1.0.zip (216K) 22 Oct 2010
• Benchmark input files in SMV format (not needed to test the tool): BioCheck_models_in_SMV (5.7M)

If you would like to obtain the sources of BioCheck or in case of difficulties with these files, please contact E. Krepska (ekr"AT"cs.vu.nl) or B. Cook (bycook"AT"microsoft.com)

Papers

BioCheck is described in a paper published at VMCAI, Jan 2011:

• B. Cook, J. Fisher, E. Krepska, N. Piterman, Proving stabilization of biological systems, In (R. Jhala and D. Schmidt, eds.) Proc. 12th Verification, Model Checking and Abstract Interpretation Conference VMCAI'11, LNCS vol. 6538, pp 134-149, 2011. PDF.
  (Appendix in the form of the Technical Report IR-CS-63 PDF)

Credits

BioCheck was created at Microsoft Research Cambridge, UK, by: Elzbieta Krepska working with Byron Cook, Nir Piterman and Jasmin Fisher.


Oct 22, 2010