BioLab

<title>bio-lab</title>
<h1>BioLab</h1>
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.
<p>You can download BioLab for Mac OS X <a href="biolab2RC1.zip">here</a>.   After downloading it, just unzip it. BioLab is pre-installed; you can run it   immediately, using the following instructions.
<h3>Defining Linear Temporal Logic Properties for BioLab</h3>
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).
<p>The syntax for the LTL formulae:
<ul>
  <li>"{" &lt;variable&gt; &lt;relop&gt; &lt;constant&gt; "}" - a relational   expression:
    <ul>
        <li>&lt;variable&gt; is a variable name, either the name "time" or the name of   an observable in the BioNetGen model;
        <li>&lt;relop&gt; is a relational operator (&lt;, &lt;=, =, &gt;, &gt;=);
        <li>&lt;constant&gt; is any constant expression legal in the C programming   language. </li>
    </ul>
    The entire expression must be contained in the curly braces.
  <li>f AND g - both f and g are true: f and g are any negation normal LTL   formulas
  <li>f OR g - either f or g is true: f and g are any negation normal LTL formulas
  <li>NOT f - F is not true: f is any negation normal LTL formula
  <li>"[" f U g "]" - read "f until g": f and g are negation normal LTL formulas.   The entire expression must be contained in square brackets.
  <li>G f - globally "f": f is any negation normal LTL formula
  <li>F f - eventually "f": f is any negation normal LTL formula </li>
</ul>
<h3>The BioNetGen Model</h3>
The BioNetGen model should contain the following   commands:
<ul>
  <li>generate_network({overwrite=&gt;1});</li>
  <li>simulate_ssa({suffix=&gt;ssa,t_end=&gt;&lt;end-time&gt;,n_steps=&gt;&lt;steps&gt;}); </li>
</ul>
<p>The only parts of this that you should change are &lt;end-time&gt; and   &lt;steps&gt;
<ul>
  <li>&lt;end-time&gt; - the end time for the simulation
  <li>&lt;steps&gt; - the number of discrete steps from time 0 to the end time </li>
</ul>
<h3>Running BioLab</h3>
The command line for running BioLab is:<br>
<p>./BioLab &lt;model-file&gt; &lt;property-file&gt; &lt;Type-I error&gt;   &lt;Type-II error&gt; &lt;Probability-Threshold&gt; &lt;BayesFactor&gt;   &lt;Number of Variables in Data File&gt; &lt;Number of Time Points in Data   File&gt; &lt;Beta-Prior Shape Parameter 1&gt; &lt;Beta-Prior Shape Parameter   2&gt;
<p>The parameters are:
<ul>
  <li>&lt;model-file&gt; a file containing a BioNetGen model
  <li>&lt;property-file&gt; a file containing a negative normal LTL model
  <li>&lt;Type-I error&gt; acceptable probability of rejecting the hypothesis when   it is true
  <li>&lt;Type-II error&gt; acceptable probability of accepting the hypothesis   when it is false, must be the same as &lt;Type-I error&gt;
  <li>&lt;Probability-Threshold&gt; the threshold probability used in the   hypothesis
  <li>&lt;BayesFactor&gt; Must be the inverse of the &lt;Type-I error&gt;
  <li>&lt;Number of Variables in Data File&gt; one more than the number of   observables in the model (because time is treated as a variable)
  <li>&lt;Number of Time Points in Data File&gt; number of steps (nsteps parameter   in simulate_ssa)
  <li>&lt;Beta-Prior Shape Parameter 1&gt; must be 1
  <li>&lt;Beta-Prior Shape Parameter 2&gt; must be 1 </li>
</ul>
<p>
    
</p>