BioModel Engineering for Systems and Synthetic Biology
Lab 2

David Gilbert
Centre for Systems and Synthetic Biology
Brunel University, London, UK


Pratical exercises for Workshop on"BioModel Engineering for Systems and Synthetic Biology" at Modelling in systems biology and synthetic biology (1-14 July 2012).

Aim

The aim of this laboratory is to enable you to gain experience with model checking of biochemical pathways for both continuous and stochastic models.

Setting up

Example files

These can be found here for the RKIP example.

Exercises

  1. Obtain a simulation run from your continuous MA1 enzymatic reaction model.
    Design four PLTLc statements, each of which should exclusively describe the behaviour of the Your statements should be descriminatory -- i.e. each statement should only describe the behaviour of the target species (probability=1), and not any of the other 3 species (probability=0).

  2. Apply your PLTLc statements to check the behaviour of your stochastic MA1 model. Make sure that you understand what the results mean this time.

  3. Try model checking your MA2 and MA3 models (continuous and stochastic).

  4. Note: if you have problems with generating the data and queries for the RKIP example, then you can find some suitable files here.

  5. Here is a Petri net model in Snoopy format for negative feedback loop amplifier signal transduction pathway. It is supposed to exhibit oscillations.
    Can you design PLTLc queries to check that this behaviour occurs? (Hint - you will need to increase the simulation time to observe the oscillations...).
    You will need to download the files to disc, don't try to view them in your browser: The model is that of Kholodenko, from
    Kholodenko BN.,
    Negative feedback and ultrasensitivity can bring about oscillations in the mitogen-activated protein kinase cascades.
    Eur J Biochem. 2000 Mar;267(6):1583-8.
    http://www.ncbi.nlm.nih.gov/pubmed/10712587.