Overview

MC2(PLTLc) is a Monte Carlo Model Checker for properties written in Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc).  The model checker takes as input a set of traces in the form of a simulation output file.  It also takes as input a query file containing a list of PLTLc properties, and returns for each property the probability that the set of traces satisfies the property.  MC2(PLTLc) can also calculate the probabilistic domains of free variables within a property;  thus it is easy to calculate the distribution of features, such as times at which peaks occur.  MC2(PLTLc) can operate with stochastic/deterministic simulation output, deterministic parameter scan output or even wet-lab data.  MC2(PLTLc) was developed at the Bioinformatics Research Centre in the University of Glasgow.

Features

The main features of MC2(PLTLc) are:

      * Logic:  Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc).

      * Model Checking:  Monte Carlo approximation through a finite number of finite traces.

      * Probabilistic Domains:  Computation of probabilistic domains of free variables in a PLTLc property.

      * Off-line approach:  Any simulation output can be used, e.g. output from ODEs, SDEs, CTMC, Gillespie.

      * Parallelisable:  Traces can be evaluated in parallel, hence distributed computation.

      * Parameter Scan:  Model checking over simulations with varying model parameters (initial concentrations or kinetic rate constants).

     * Integrations:  Able to read simulation output from Snoopy, Gillespie2, BioNessie and BioNessie Lite.

Download

The latest MC2(PLTLc) package released 27th April, 2008 can be downloaded:  MC2 v2.0 Beta 2.

This package contains:

     * gillespie0.11-modified/ - The modified Gillespie2 v0.1.1 source providing exact Gillespie simulation with optimised output files. Please recompile to generate for your system architecture.

     * models/ - The Kholodenko, Levchenko and TwoReactionModel models.  Stochastic models are indicated with the filename suffix: _#MOLECULES).

     * queries/ - Example query files for use with MC2(PLTLc) and a unix script to create the S1 query for higher numbers of levels.

     * simulation_outputs/ - Example simulation outputs for use with MC2(PLTLc).

     * gillespie2-levchenko_4.run, gillespie2-tworeactionmodel_10.run - Example run commands for the modified Gillespie2 simulator to produce a file of 1,000 traces.

     * MC2v2.0beta2.jar - MC2(PLTLc) v2.0 Beta 2 compiled with Java v1.5.

     * MC2.run - Example run commands for MC2(PLTLc), checking the three types of outputs; deterministic, stochastic and deterministic parameter scan.

     * UserManual.pdf - The user manual for MC2(PLTLc), explaining how to install and run the various simulators and perform model checking.

Contact

For any comments, suggestions or technical problems, please e-mail:  radonald@brc.dcs.gla.ac.uk.  MC2(PLTLc) author:  Robin Donaldson.

Last updated:  27th April, 2008