BioLab

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:

"{" <variable> <relop> <constant> "}" - a relational expression:
- <variable> is a variable name, either the name "time" or the name of an observable in the BioNetGen model;
- <relop> is a relational operator (<, <=, =, >, >=);
- <constant> is any constant expression legal in the C programming language.
The entire expression must be contained in the curly braces.
f AND g - both f and g are true: f and g are any negation normal LTL formulas
f OR g - either f or g is true: f and g are any negation normal LTL formulas
NOT f - F is not true: f is any negation normal LTL formula
"[" f U g "]" - read "f until g": f and g are negation normal LTL formulas. The entire expression must be contained in square brackets.
G f - globally "f": f is any negation normal LTL formula
F f - eventually "f": f is any negation normal LTL formula

The BioNetGen Model

The BioNetGen model should contain the following commands:

generate_network({overwrite=>1});
simulate_ssa({suffix=>ssa,t_end=><end-time>,n_steps=><steps>});

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

<end-time> - the end time for the simulation
<steps> - the number of discrete steps from time 0 to the end time

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:

<model-file> a file containing a BioNetGen model
<property-file> a file containing a negative normal LTL model
<Type-I error> acceptable probability of rejecting the hypothesis when it is true
<Type-II error> acceptable probability of accepting the hypothesis when it is false, must be the same as <Type-I error>
<Probability-Threshold> the threshold probability used in the hypothesis
<BayesFactor> Must be the inverse of the <Type-I error>
<Number of Variables in Data File> one more than the number of observables in the model (because time is treated as a variable)
<Number of Time Points in Data File> number of steps (nsteps parameter in simulate_ssa)
<Beta-Prior Shape Parameter 1> must be 1
<Beta-Prior Shape Parameter 2> must be 1