BioModel Engineering for Systems and Synthetic Biology
Lab 2

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

Exercises

Setting up

• Ensure that you have installed MC2, Snoopy and Java on your computer.

• Exporting traces from Snoopy:
  • For deterministic models, select 'Direct export'.
  • For stochastic models, select 'Exact trace export'.
  • Then select destination, file name and file type under Properties. Note you must give the extension to the file (i.e. '.csv').
  • Select the separator to be a semi-colon.
  • Perform the simulation.

• PLTLc properties
  

  G (P) : P always happens
  F (P) : P happens at some time
  X (P) : P happens in the next time point
  P1 U P2 : P1 happens until P2 happens
  

  Examples:
  Protein stability:
  P=? [ time >= 100 -> ([Protein] >= 4 ^ [Protein] <= 6) ]
  

  Protein rises to a maximum and then remains constant:
  P=? [ (d[Protein] > 0) U ( G([Protein] >= 0.99*max[Protein]) ) ]
  

  Using an editor, you will need to create a text file file of PLTLc properties to model check. The file can contain any number of such properties, each on one line, where the format of the line is:
  P=? PROPERTY
  e.g. (can you understand what this property means?)
  P=?[G(d[A]>0)]

• Running the model checker
  Open a command window on your computer.
• Ensure that you have the trace file that you generated from Snoopy (e.g. deterministic_trace.csv), the text file of PLTLc properties (e.g. my_deterministic_properties.txt), and the MC2 software in the same folder, and change to that folder.
• Perform model checking with mc2 by issuing the following command at the command line, using the 'stoch' option and the '-snoopy' final flag, for both deterministic as well as stochastic models, e.g.:

  java -jar MC2v2.0beta2.jar stoch deterministic_trace.csv my_deterministic_properties.txt -snoopy
  

  or

  java -jar MC2v2.0beta2.jar stoch stochastic_trace.csv my_stochastic_properties.txt -snoopy

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
   • Substrate
   • Product
   • Enzyme
   • Substrate-enzyme complex
   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).
   • Apply your PLTLc statements that you developed for the MA1 model to check the behaviour of your MA2 and MA3 models (both stochastic and continuous). Do the statements still correctly describe the behaviour of the 4 species from MA1?
   • Design statements to describe the behaviour of the enzyme-product complex -- can you use the same statements for MA2 and MA3?

4. Obtain a continuous model of the RKIP pathway.
   Design and apply PLTLc statements to describe the behaviour of each of the species.

5. Obtain a stochastic model of the RKIP pathway.
   Design and apply PLTLc statements to describe the behaviour of each of the species. Can you use similar statements to those for the deterministic model?

6. 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:
   • Continuous version here
   • Stochastic version here
   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.