Lecture 17: Compartments in BioPEPA

18 March 2010

Working through the following paper:

  • Federica Ciocchetta and Maria Luisa Guerriero. Modelling Biological Compartments in Bio-PEPA, in MeCBIC 2008: Proceedings of the Second International Meeting on Membrane Computing and Biologically Inspired Process Calculi. Electronic Notes in Theoretical Computer Science 227:77–95, January 2009.

Adding compartments to BioPEPA: syntax; compositional operational semantics; structured locations including compartments, membranes, and the boundaries between them; appropriate kinetics; sample model of intracellular calcium oscillations.

Homework

Please fill out and submit an anonymous feedback questionnaire. Thank you.


Lecture 16: Modelling tools for Bio-PEPA

16 March 2010

Guest lecture by Stephen Gilmore explaining and demonstrating the BioPEPA tools, principally the Eclipse plugin.


Lecture 15: Process Algebras for Systems Biology

11 March 2010

Background on process algebras / process calculi: what they can be useful for, and various domains where they have been applied. Specific applications to systems biology; and the wide range of process calculi proposed for different aspects of biological systems.

Brief introduction to PEPA and BioPEPA, with reference to Ciocchetta and Hillston (2009).

Link: Slides.


Lecture 14: Continuous Petri Nets and Differential Equations

8 March 2010

Moving from discrete events to continuous flow: semantics of continuous Petri nets; correspondence with chemical reaction equations; deriving ordinary differential equations (ODEs); conservation laws, equilibria, numerical solutions and trajectories through phase space. Relating transition rates for discrete events to reaction rates for continuous flow; dependence on reaction stoichiometry.

Some examples, including derivation of Michaelis-Menten semantics.

Thursday’s lecture will be an introduction to BioPEPA, followed by Stephen Gilmore on Monday.

Link: Slides.

Homework

Read §§6–9 of Heiner et al., and §§1–4 of Ciocchetta and Hillston, on BioPEPA.

This earlier paper by Gilbert and Heiner also explains modelling biological processes with continuous Petri nets.


Lecture 13: More Stochastic Kinetics

5 March 2010

More on Gillespie’s algorithm for stochastic simulation, including the remainder of the slides from Gillespie’s invited CMSB talk. Various tau-leaping methods to more efficiently simulate larger systems; concerns about bounding the errors in these approximate techniques. Further approximation with continuous models, still stochastic, and then by deterministic systems of differential equations for even large scales.

This is discussed in Chapter 8 of Wilkinson’s book on stochastic modelling.

You can also read Gillespie’s own papers on this: his original SSA proposal, and a more recent survey of progress since then.

Return of coursework, and discussion of some particular issues.

  • Reachability graph for the repressilator model.
  • Drawing subnets arising from transition and place invariants.
  • Eight minimal place invariants for the ECA synthesis network; invariants for preservation of uridine, saccharide, phosphate and undecaprenyl groups.
  • Logical formulae in LTL, CTL and HML: decoding and coding them.
  • The until connective denotes that the statement will eventually hold; release may not.
  • HML must modality [a]p means that if a happens, p is then true — but it doesn’t say anything about whether a does happen, or is even possible.

Any more questions or answers about the coursework, please post on the comments below.


Lecture 12: Large Systems and Stochastic Kinetics

2 March 2010

Revisiting Kwiatkowska et al. on probabilistic model-checking for systems biology. Moving from models of a single protein to slightly larger populations, still with symbolic model-checking.

The problem of state-space explosion, and the use of simulation. Gillespie’s algorithm for stochastic simulation. I’m using the slides from Gillespie’s invited talk at CMSB 2007 in Edinburgh. So far we have covered the approximation from precise dynamic simulation of all positions and velocities, down to stochastic simulation of populations through modelling only reactive molecular collisions. This gives the exact SSA; next are various tau-leaping methods for efficient approximation.

Wilkinson’s book on stochastic modelling covers the Gillespie algorithm in §§6.2–6.5, with Chapter 8 then going on to deal with approximation strategies.

Links: Slides; Gillespie on Stochastic Chemical Kinetics; All CMSB 2007 talks.


Lecture 11: Markov Chains and Stochastic Logics

18 February 2010

Small Petri net example in the form of a signal cascade. Extracting from this in turn: a transition system; a DTMC with transition probabilities; and a CTMC with rates. Corresponding refinements of temporal logic: LTL/CTL; PCTL with probabilities; CSL with probabilities and duration. How this extends expressiveness, and how replacing discrete “always” with probabilistic “almost surely” gives results more closely matching intuition.

Probabilistic symbolic model checking and the PRISM tool. Examples from:

Homework

Read the remainder of the Kwiatkowska et al. tutorial, §§4–6.

Also, recall this short report:

In the meantime, however, Fisher and her fellow executable-biology enthusiasts have a lot of convincing to do, says Stephen Oliver, a biologist at the University of Cambridge, UK. “Modelling in general is regarded sceptically by many biologists,” he points out.

Do you think this is true? Can you find any evidence for or against?


Lecture 10: Stochastic Petri Nets and Markov Chains

11 February 2010

Introducing probability to Petri nets through continuous time and transition firing rates. Markov chains, and variations thereon: Discrete Time Markov Chains (DTMC); Markov decision procedures (MDP); Continuous Time Markov Chains (CTMC). How this last one is appropriate to capture the behaviour of a stochastic Petri net. Brief mention of the PRISM probabilistic model checker.

Link: Slides

Homework

Read §§1–3 of this tutorial article.

Assignment

The first assignment is now out. See the coursework web page for more information.


Lecture 9: Continuous time

8 February 2010

Note: The slides have been revised since the lecture, removing some untruths, adding more about BDDs and exponential distribution, and providing further references.

Symbolic Model Checking: How advanced algorithms test assertions on systems with states than you can imagine possible.

Road Map Review: Shifting between high-level intuitive models and low-level mathematical ones, with multiple choices and analyses.

Continuous Time: Negative exponential distributions and why we use it; starting with Stochastic Petri Nets.

Link: Slides (updated)

Homework

Read the following short articles for Thursday.


Lecture 8: Mix, match and use temporal logics

6 February 2010

Revisit example valuation of CTL formula, now corrected. Further possible logics: Hennessy-Milner, modal μ-calculus, and monadic second-order logic. Presentation of syntax, semantics, and small examples. Relative expressiveness. Mixing and matching modalities and operators for convenience, distinct from expressiveness: CTL- as an example.

Application to specific biological models, as discussed in these articles: Fages and Rizk evaluating LTL formulae over time series data; de Jong et al. on mapping textual descriptions into CTL.

Link: Slides