BioLab is a stochastic model-checker for BioNetGen models. You provide, as input to BioLab, a BioNetGen model, a property expressed in linear temporal logic, and a probability. BioLab tells you whether the property is satisfied with probability less than the given probability or greater than the given probability.

You can download BioLab for Mac OS X here. After downloading it, just unzip it. BioLab is pre-installed; you can run it immediately, using the following instructions.

Defining Linear Temporal Logic Properties for BioLab

Linear Temporal Logic (LTL) formulas must be in negation normalized form to be interpreted correctly by BioLab (i.e., negations are pushed inside as far as possible).

The syntax for the LTL formulae:

The BioNetGen Model

The BioNetGen model should contain the following commands:

The only parts of this that you should change are <end-time> and <steps>

Running BioLab

The command line for running BioLab is:

./BioLab <model-file> <property-file> <Type-I error> <Type-II error> <Probability-Threshold> <BayesFactor> <Number of Variables in Data File> <Number of Time Points in Data File> <Beta-Prior Shape Parameter 1> <Beta-Prior Shape Parameter 2>

The parameters are: